Occurrence Tree Automorphisms

Extension Name: preserve.th

Primitive Lexicon:

Relations:

(ubiquitous ?a1 ?a2)

Defined Lexicon:

Relations:

(end_iso ?s1 ?s2 ?s3 ?s4)

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

Definitional Extensions Required by this Extension: occ_precond.def

Axioms

Axiom 1

(forall (?a1 ?a2 ?s1 ?s2)
	(if	  (and	(ubiquitous ?a1 ?a2)
			(min_precedes ?s1 ?s2 ?a2))
		  (exists (?s3 ?s4 ?s5 ?s6)
			(and	(tree_equiv ?s1 ?s2)
				(tree_equiv ?s3 ?s4)
				(occurrence_of ?s5 ?a1)
				(occurrence_of ?s6 ?a1)
				(legal_equiv ?s5 ?s6)
				(end_iso ?s3 ?s4 ?s5 ?s6)))))

Axiom 2

(forall (?a1 ?a2 ?s1 ?s2)
	(if	  (and	(ubiquitous ?a1 ?a2)
			(min_precedes ?s1 ?s2 ?a2))
		  (not (exists (?s3 ?s4)
			(and	(occurrence_of ?s3 ?a1)
				(occurrence_of ?s4 ?a1)
				(legal_equiv ?s3 ?s4)
				(end_iso ?s1 ?s2 ?s3 ?s4))))))

Axiom 3

(forall (?a1 ?a2 ?s1 ?s2 ?s3 ?s4)
	(if	  (and	(ubiquitous ?a1 ?a2)
			(occurrence_of ?s3 ?a1)
			(occurrence_of ?s4 ?a1)
			(legal_equiv ?s3 ?s4)
			(end_iso ?s1 ?s2 ?s3 ?s4))
		  (exists (?o1 ?o2)
			(and	(occurrence_of ?o1 ?a1)
				(occurrence_of ?o2 ?a1)
				(subactivity_occurrence ?s1 ?o1)
				(subactivity_occurrence ?s2 ?o1)))))

Definitions

Definition 1

(forall (?s1 ?s2 ?s3 ?s4) (iff (end_iso ?s1 ?s2 ?s3 ?s4)
(exists (?s5 ?s6)
	(and	(precedes ?s5 ?s1)
		(precedes ?s5 ?s3)
		(precedes ?s6 ?s2)
		(precedes ?s6 ?s4)
		(tree_equiv ?s1 ?s2)
		(tree_equiv ?s3 ?s4)
		(tree_equiv ?s5 ?s6)))))