Branch Structure and Ordering

Branch Structure and Ordering

Extension Name: ordered.def

Primitive Lexicon: None

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: None

Grammar: ordered.bnf

Definitions

Definition 1 The subtree rooted in ?s1 can be monomorphically embedded into the subtree rooted in ?s2. 
(forall (?s1 ?s2 ?a) (iff (mono_tree ?s1 ?s2 ?a) 
(forall (?s3 ?s4 ?s5)
	(if	  (and	(min_precedes ?s1 ?s3 ?a)
			(min_precedes ?s2 ?s4 ?a)
			(mono ?s3 ?s4 ?a)
			(min_precedes ?s3 ?s5 ?a))
		  (exists (?s6)
			(and	(mono ?s5 ?s6 ?a)
				(min_precedes ?s4 ?s6 ?a)))))))
Definition 2 This relation holds iff there exists an order automorphism that maps the subtree rooted in ?s1 to the subtree rooted in ?s2. 
(forall (?s1 ?s2 ?a) (iff (order_tree ?s1 ?s2 ?a)
(and	(mono_tree ?s1 ?s2 ?a)
	(forall (?s3 ?s4 ?s5 ?s6)
		(if	  (and	(min_precedes ?s1 ?s3 ?a)
				(min_precedes ?s2 ?s4 ?a)
				(cousin ?s3 ?s4 ?a)
				(min_precedes ?s3 ?s5 ?a)
				(cousin ?s5 ?s6 ?a))
			  (iff	(iso_occ ?s3 ?s5 ?a)
				(iso_occ ?s4 ?s6 ?a)))))))
Definition 3 Two activity occurrences are root automorphic iff there exist atomic subactivity occurrences of each activity occurrence that are the roots of isomorphic subtrees. 
(forall (?occ1 ?occ2) (iff (root_automorphic ?occ1 ?occ2) 
(exists (?a ?s1 ?s2)
	(and	(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)
		(subactivity_occurrence ?s1 ?occ1)
		(subactivity_occurrence ?s2 ?occ2)
		(order_tree ?s1 ?s2 ?a)
		(order_tree ?s2 ?s1 ?a)))))
Definition 4 An activity occurrence is ordered iff it is root automorphic with every other activity occurrence in the same tree. 
(forall (?occ1) (iff (ordered ?occ1) 
(forall (?occ2)
	(if	  (same_grove ?occ1 ?occ2)
		  (root_automorphic ?occ1 ?occ2)))))
Definition 5 An activity occurrence is nondeterministically ordered iff each activity occurrence in the same tree is root automorphic to some other activity occurrence in the same tree. 
(forall (?occ1) (iff (nondet_ordered ?occ1)
(forall (?occ2)
	(if	  (same_grove ?occ1 ?occ2)
		  (exists (?occ3)
			(and	(same_grove ?occ1 ?occ3)
				(not (= ?occ3 ?occ2))
				(root_automorphic ?occ2 ?occ3)))))))
Definition 6 An activity is broken ordered iff there exist activity occurrences in the same tree that are root automorphic to some other activity occurrences in the same tree, and there also exist activity occurrences in same tree that are not root automorphic to any other activity occurrence. 
(forall (?occ1) (iff (broken_ordered ?occ1)
(exists (?occ2)
	(and	(same_grove ?occ1 ?occ2)
		(not (= ?occ1 ?occ2))
		(root_automorphic ?occ1 ?occ2)
		(forall (?occ3)
			(if	  (and	(same_grove ?occ3 ?occ1)
					(not (= ?occ3 ?occ2)))
				  (not (root_automorphic ?occ3 ?occ2))))))))
Definition 7 An activity occurrence is unordered iff none of the activity occurrences in the same tree are root automorphic. 
(forall (?occ1) (iff (unordered ?occ1)
(forall (?occ2)
	(if	  (and	(same_grove ?occ1 ?occ2)
			(not (= ?occ1 ?occ2)))
		  (not (root_automorphic ?occ1 ?occ2))))))