Preconditions

Preconditions for Activities

Extension Name: precond.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

Theories Required by this Extension: disc_state.th, occtree.th, psl_core.th

Definitional Extensions Required by this Extension: none

Grammar: precond.bnf

Definitions

Definition 1 Two atomic activity occurrences are legal equivalent with respect to an activity iff the two occurrences agree on their membership in the legal occurrence tree. 
(forall (?s1 ?s2) (iff (legal_equiv ?s1 ?s2)
(iff    (legal ?s1)
        (legal ?s2))))
Definition 2 Two activity occurrences are precondition equivalent with respect to an activity iff the two occurrences agree on the legality of the occurrences of the activity. 
(forall (?a ?s1 ?s2) (iff (poss_equiv ?a ?s1 ?s2)
(if	  (and	(occurrence_of ?s1 ?a)
		(occurrence_of ?s2 ?a))
	  (legal_equiv ?s1 ?s2))))
Definition 3 An activity is unconstrained iff all activity occurrences in the occurrence tree are precondition equivalent. 
(forall (?a) (iff (unconstrained ?a)
(forall (?s1 ?s2)
	(if	  (and	(activity_occurrence ?s1)
			(activity_occurrence ?s2))
		  (poss_equiv ?a ?s1 ?s2)))))
Definition 4 An activity ?a is partially constrained iff all occurrences of certain activities within the occurrence tree are precondition equivalent with respect to ?a. 
(forall (?a) (iff (partial_constrained ?a)
(and	(exists (?a1)
		(forall (?s1 ?s2)
			(if	  (and	(occurrence_of ?s1 ?a1)
					(occurrence_of ?s2 ?a1))
				  (poss_equiv ?a ?s1 ?s2))))
	(exists (?a2 ?s3 ?s4)
		(and	(occurrence_of ?s3 ?a2)
			(occurrence_of ?s4 ?a2)
			(not (poss_equiv ?a ?s3 ?s4)))))))
Definition 5 An activity ?a is constrained iff every activity has occurrences that are not precondition equivalent with respect to ?a. 
(forall (?a) (iff (constrained ?a)
(forall (?a1)
	(exists (?s1 ?s2)
		(and	(occurrence_of ?s1 ?a1)
			(occurrence_of ?s2 ?a1)
			(not (poss_equiv ?a ?s1 ?s2)))))))