Temporal Preconditions

Extension Name: time_precond.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

(begin_equiv ?s1 ?s2)
(time_precond ?a)
(partial_time ?a)
(rigid_time ?a)

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

Definitional Extensions Required by this Extension: precondition.def, start.def

Grammar: time_precond.bnf

Definitions

Definition 1 Two atomic activity occurrences are begin-equivalent if and only if they have equal beginof timepoints.

(forall (?s1 ?s2) (iff (begin_equiv ?s1 ?s2)
(= (beginof ?s1) (beginof ?s2))))

Definition 2 An activity is a time precondition activity iff whenever two atomic occurrences in the occurrence tree agree on their beginof timepoints, then they agree on the extension of poss for the activity.

(forall (?a) (iff (time_precond ?a)
(forall (?s1 ?s2)
	(if	  (begin_equiv ?s1 ?s2)
                  (poss_equiv ?a ?s1 ?s2)))))

Definition 3 An activity is a partially temporally constrained activity if and only if there exist occurrence-preserving automorphisms

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

Definition 4 An activity is a rigid time activity if and only if the only occurrence-preserving timeline automorphism is the trivial one.

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