Iterated Occurrence Ordering

Iterated Occurrence Ordering

Extension Name: ioo.th

Primitive Lexicon:

Relations:

Defined Lexicon:

Relations:

Theories Required by this Extension: act_occ.th, complex.th, atomic.th, subactivity.th, occtree.th, psl_core.th

Definitional Extensions Required by this Extension: repetitive.def

Axioms

Axiom 1 If the atomic subactivity occurrence ?s is the maximal root of a repeated subtree with respect to ?occ, then the iterated occurrence ordering relation rep_precedes is isomorphic to the repeated subtree. 
(forall (?s1 ?occ ?a)
	(if	  (and	(occurrence_of ?occ ?a)
			(max_reptree ?s1 ?occ))
		  (forall (?s2)
			(iff	(min_precedes ?s1 ?s2 ?a)
				(rep_precedes ?s1 ?s2 ?a)))))
Axiom 2 Every atomic subactivity occurrence in the iterated occurrence ordering is an element of a repeated subtree. 
(forall (?s1 ?s2 ?a)
	(if	  (rep_precedes ?s1 ?s2 ?a)
		  (exists (?occ1 ?occ2 ?s3)
			(and	(occurrence_of ?occ1 ?a)
				(same_grove ?occ1 ?occ2)
				(subactivity_occurrence ?s1 ?occ1)
				(reptree ?s2 ?occ2)
				(min_precedes ?s3 ?s1 ?a)))))

Definitions

Definition 1 The atomic subactivity occurrence ?s is the root of a repeated subtree with respect to ?occ, and there does not exist any later atomic subactivity occurrence on the same branch as ?s that is also the root of a repeated subtree. 
(forall (?s ?occ) (iff (max_reptree ?s ?occ)
(and	(reptree ?s ?occ)
	(forall (?s1 ?a)
		(if	  (and	(occurrence_of ?occ ?a)
				(min_precedes ?s ?s1 ?a))
			  (not (reptree ?s1 ?occ)))))))