Time-based Duration

Time-based Duration

Extension Name: time_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, time_precond.def

Grammar: time_dur.bnf

Definitions

Definition 1 An activity is a rushhour activity iff whenever two occurrences agree on their beginof timepoints, then they agree on duration. 
(forall (?a) (iff (rushhour ?a) 
(forall (?occ1 ?occ2)
        (if	  (and	(occurrence_of ?occ1 ?a)
			(occurrence_of ?occ2 ?a)
			(begin_equiv ?occ1 ?occ2))
                  (dur_equiv ?occ1 ?occ2)))))
Definition 2 An activity is a weekend activity if and only if there exist duration-preserving beginof automorphisms. 
(forall (?a) (iff (weekend ?a) 
(and 	(exists (?occ1) 
		(forall (?occ2)
			(if	  (and	(occurrence_of ?occ1 ?a)
					(occurrence_of ?occ2 ?a)
					(begin_equiv ?occ1 ?occ2))
				  (dur_equiv ?occ1 ?occ2))))
	(exists (?occ3 ?occ4)
		(and	(occurrence_of ?occ3 ?a)
			(occurrence_of ?occ3 ?a)
			(begin_equiv ?occ3 ?occ4)
			(not (dur_equiv ?occ3 ?occ4)))))))
Definition 3 An activity is a gridlock activity if and only if the only duration-preserving beginof automorphism is the trivial one. 
(forall (?a) (iff (gridlock ?a) 
(forall (?occ1)
	(if	  (occurrence_of ?occ1 ?a)
		  (exists (?occ2)
			(and	(occurrence_of ?occ2 ?a)
				(begin_equiv ?occ1 ?occ2)
				(not (dur_equiv ?occ1 ?occ2))))))))