Preconditions based on State and Time

Extension Name: mixed_precond.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

(mixed_precond ?a)
(partial_mixed ?a)
(rigid_mixed ?a)

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

Definitional Extensions Required by this Extension: state_precond.def, time_precond.def

Grammar: mixed_precond.bnf

Definitions

Definition 1 An activity is a mixed preconditional activity iff whenever two occurrences agree on state and their beginof timepoints, then they agree on the extension of poss for the activity.

(forall (?a) (iff (mixed_precond ?a)
(forall (?s1 ?s2)
        (if	  (and	(state_equiv ?s1 ?s2)
			(begin_equiv ?s1 ?s2))
                  (poss_equiv ?a ?s1 ?s2)))))

Definition 2 An activity is a partially mixed constrained activity if and only if there exist occurrence-preserving automorphisms.

(forall (?a) (iff (partial_mixed ?a)
(and    (exists (?s1)
                (forall (?s2)
                        (if	  (and	(state_equiv ?s1 ?s2)
					(begin_equiv ?s1 ?s2))
                                  (poss_equiv ?a ?s1 ?s2))))
        (exists (?s3 ?s4)
                (and    (state_equiv ?s3 ?s4)
			(begin_equiv ?s3 ?s4)
                        (not (poss_equiv ?a ?s3 ?s4)))))))

Definition 3 An activity is a rigid mixed activity if and only if the only occurrence-preserving automorphism that is both a fluent automorphism and a timeline automorphism, is the trivial one.

(forall (?a) (iff (rigid_mixed ?a)
(forall (?s1)
        (exists (?s2)
                (and    (state_equiv ?s1 ?s2)
			(begin_equiv ?s1 ?s2)
                        (not (poss_equiv ?a ?s1 ?s2)))))))