State-based Preconditions

State-based Preconditions

Extension Name: state_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: precond.def

Grammar: state_precond.bnf

Definitions

Definition 1 Two activity occurrences are state equivalent iff the same states hold after the occurrences. 
(forall (?s1 ?s2) (iff (state_equiv ?s1 ?s2)
(forall (?f)
	(iff    (prior ?f ?s1)
                (prior ?f ?s2)))))
Definition 2 An activity is a markov preconditional activity iff whenever two occurrences agree on state, then they agree on the extension of poss for the activity. 
(forall (?a) (iff (markov_precond ?a)
(forall (?s1 ?s2)
        (if	  (state_equiv ?s1 ?s2)
                  (poss_equiv ?a ?s1 ?s2)))))
Definition 3 An activity is a partially state constrained activity if and only if there exist occurrence-preserving fluent automorphisms. 
(forall (?a) (iff (partial_state ?a)
(and 	(exists (?s1) 
		(forall (?s2)
			(if	  (state_equiv ?s1 ?s2)
				  (poss_equiv ?a ?s1 ?s2))))
	(exists (?s3 ?s4)
		(and	(state_equiv ?s3 ?s4)
			(not (poss_equiv ?a ?s3 ?s4)))))))
Definition 4 An activity is a rigid state activity if and only if the only occurrence-preserving fluent automorphism is the trivial one. 
(forall (?a) (iff (rigid_state ?a)
(forall (?s1)
	(exists (?s2)
		(and	(state_equiv ?s1 ?s2)
			(not (poss_equiv ?a ?s1 ?s2)))))))