State-based Duration

State-based Duration

Extension Name: state_dur.def

Primitive Lexicon: None

Defined Lexicon:

Relations:

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

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

Grammar: state_dur.bnf

Definitions

Definition 1 An activity is a conditional duration activity iff whenever two occurrences agree on state, then they agree on duration. 
(forall (?a) (iff (conditional_duration ?a) 
(forall (?occ1 ?occ2)
        (if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(state_equiv ?occ1 ?occ2))
                  (dur_equiv ?occ1 ?occ2)))))
Definition 2 An activity is a context duration activity if and only if there exist duration-preserving fluent automorphisms. 
(forall (?a) (iff (context_duration ?a) 
(and 	(exists (?occ1) 
		(forall (?occ2)
			(if	  (and	(occurrence_of ?occ1 ?a)
					(occurrence_of ?occ2 ?a)
					(state_equiv ?occ1 ?occ2))
				  (dur_equiv ?occ1 ?occ2))))
	(exists (?occ3 ?occ4)
		(and	(occurrence_of ?occ3 ?a)
			(occurrence_of ?occ3 ?a)
			(state_equiv ?occ3 ?occ4)
			(not (dur_equiv ?occ3 ?occ4)))))))
Definition 3 An activity is an unconditional duration activity if and only if the only duration-preserving fluent automorphism is the trivial one. 
(forall (?a) (iff (unconditional_duration ?a) 
(forall (?occ1)
	(if	  (occurrence_of ?occ1 ?a)
		  (exists (?occ2)
			(and	(occurrence_of ?occ2 ?a)
				(state_equiv ?occ1 ?occ2)
				(not (dur_equiv ?occ1 ?occ2))))))))