Compacting Branch Structure

Compacting Branch Structure

Extension Name: compacted.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: permute.def

Grammar: compacted.bnf

Definitions

Definition 1 An activity is compacted iff there exists a branch such that the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on the first branch. 
(forall (?a) (iff (compacted ?a)
(exists (?occ1)
	(and	(occurrence_of ?occ1 ?a)
		(forall (?occ2)
			(if	  (and	(occurrence_of ?occ2 ?a)
					(not (same_grove ?occ1 ?occ2)))
				  (branch_homomorphic ?occ1 ?occ2)))))))
Definition 2 An activity is nondeterministically compacted iff there exists a branch such that the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on the first branch. 
(forall (?a) (iff (nondet_compacted ?a)
(forall (?occ1)
	(if	  (occurrence_of ?occ1 ?a)
		  (exists (?occ2)
			(and	(occurrence_of ?occ2 ?a)
				(not (same_grove ?occ1 ?occ2))
				(branch_homomorphic ?occ1 ?occ2)))))))
Definition 3 An activity is partially compacted iff there exists a branch such that the set of atomic subactivity occurrences on each branch of the minimal activity tree is a permutation of the atomic subactivity occurrences on the first branch. 
(forall (?a) (iff (partial_compacted ?a)
(exists (?occ1 ?occ2 ?occ3)
	(and	(occurrence_of ?occ1 ?a)
		(occurrence_of ?occ2 ?a)
		(not (same_grove ?occ1 ?occ2))
		(branch_homomorphic ?occ1 ?occ2)
		(occurrence_of ?occ3 ?a)
		(same_grove ?occ3 ?occ1)
		(forall (?occ4)
			(if	  (and	(occurrence_of ?occ4 ?a)
					(not (= ?occ2 ?occ4))
					(same_grove ?occ2 ?occ4))
				  (not (branch_homomorphic ?occ2 ?occ4))))))))
Definition 4 An activity is stiff iff none of the branches in an activity tree for ?a are branch epimorphic to the branches of any other activity tree for ?a. 
(forall (?a) (if (stiff ?a)
(forall (?occ1 ?occ2)
	(if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(not (same_grove ?occ1 ?occ2)))
		  (not (branch_homomorphic ?occ1 ?occ2))))))