Duration Theory

Extension Name: duration.th

Primitive Lexicon:

Predicates:

Functions: Constants: Theories Required by this Extension: pslcore.th

Defined Lexicon:

Functions:

Definitional Extensions Required by this Extension: none

Axioms

Axiom 1 zero, max+, and max- are all timedurations. 
(and	(timeduration zero)
	(timeduration max+)
	(timeduration max-))
Axiom 2 The result of adding two timedurations is a timeduration. 
(forall (?d1 ?d2)
(if	  (and	(timeduration ?d1)
		(timeduration ?d2))
	  (timeduration (add ?d1 ?d2))))
Axiom 3 The add function is associative. 
(forall (?d1 ?d2 ?d3)
(if	  (and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
          (= (add (add ?d1 ?d2) ?d3) (add ?d1 (add ?d2 ?d3)))))
Axiom 4 zero is the additive identity. 
(forall (?d)
(if	  (timeduration ?d)
          (= (add ?d zero) ?d)))
Axiom 5 For any timeduration, there exists an additive inverse. 
(forall (?d1)
(if	  (timeduration ?d1)
          (exists (?d2)
		(and 	(timeduration ?d2)
                	(= (add ?d1 ?d2) zero)))))
Axiom 6 The add function is commutative. 
(forall (?d1 ?d2)
(if	  (and	(timeduration ?d1)
		(timeduration ?d2))
          (= (add ?d1 ?d2) (add ?d2 ?d1))))
Axiom 7 The result of multiplying a timeduration by a scalar value is a timeduration. 
(forall (?d ?r)
(if	  (timeduration ?d)
	  (timeduration (mult ?r ?d))))
Axiom 8 Multiplication by scalars: 
(forall (?d1 ?d2 ?r)
        (= (mult ?r (add ?d1 ?d2)) (add (mult ?r ?d1) (mult ?r ?d2))))
Axiom 9 
(forall (?d ?r ?s)
        (= (mult (add ?r ?s) ?d) (add (mult ?r ?d) (mult ?s ?d))))
Axiom 10 
(forall (?d ?r ?s)
        (= (mult (mult ?r ?s) ?d) (mult ?r (mult ?s ?d))))
Axiom 11 one is the multiplicative identity. 
(forall (?d)
        (= ?d (mult one ?d)))
Axiom 12 Ordering Axioms for timedurations. 
(forall (?d1 ?d2 ?d3)
(if	(and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
        (iff    (lesser ?d1 ?d2)
                (lesser (add ?d1 ?d3) (add ?d2 ?d3)))))
Axiom 13 
(forall (?d1 ?d2 ?d3)
(if	(and	(timeduration ?d1)
		(timeduration ?d2)
		(timeduration ?d3))
        (iff    (= ?d1 ?d2)
                (= (add ?d1 ?d3) (add ?d2 ?d3)))))
Axiom 14 max- is lesser than any timeduration, and max+ is greater than any timeduration. 
(forall (?d)
	(if	  (timeduration ?d)
		  (and	(lesser ?d max+)
			(lesser max- ?d))))
Axiom 15 The result of adding any duration other than max+ to max- is max-, and vice versa, the "sum" of max- and max+ is zero. 
(forall (?d)
(if	  (timeduration ?d)
	  (and 	(if	  (not (= ?d max-)) (= max+ (add ?d max+)))
		(if	  (not (= ?d max+)) (= max- (add ?d max-)))
		(= zero (add max+ max-)))))
Axiom 16 The duration function assigns a timeduration to every pair of timepoints. 
(forall (?t1 ?t2)
	(if	  (and	(timepoint ?t1)
			(timepoint ?t2))
		  (timeduration (duration ?t1 ?t2))))
Axiom 17 Every timeduration is equal to the value of the duration function for some pair of timepoints. 
(forall (?d)
	(if	  (timeduration ?d)
        	  (exists (?t1 ?t2)
			(and	(timepoint ?t1)
				(timepoint ?t2)
	                	(= ?d (duration ?t1 ?t2))))))
Axiom 18 The value of the duration function is zero if and only if the two timepoints are equal. 
(forall (?t1 ?t2)
(if	  (and	(timepoint ?t1)
		(timepoint ?t2))
	  (iff	(= zero (duration ?t1 ?t2))
		(= ?t1 ?t2))))
Axiom 19 The value of the duration function between ?t1 and ?t2 is the additive inverse of the value of the duration function between ?t2 and ?t1. 
(forall (?t1 ?t2)
(if	  (and	(timepoint ?t1)
		(timepoint ?t2))
	  (= zero (add (duration ?t1 ?t2) (duration ?t2 ?t1)))))
Axiom 20 Given a point i other than inf- or inf+, the duration from i to any point is unique. 
(forall (?t1 ?t2 ?t3)
	(if	  (and	(timepoint ?t1)
			(timepoint ?t2)
			(timepoint ?t3)
			(not (= ?t1 inf-))
			(not (= ?t2 inf+))
			(= (duration ?t1 ?t2) (duration ?t1 ?t3)))
		  (= ?t1 ?t2)))
Axiom 21 The duration from any point other than inf- to inf- is max- and from any point other than inf+ to inf+ is max+. 
(forall (?t)
(and 	(if	  (and	(timepoint ?t)
			(not (= ?t inf-)))
		  (= max+ (duration inf- ?t)))
	(if	  (and	(timepoint ?t)
			(not (= ?t inf+)))
		  (= max- (duration inf+ ?t)))))
Axiom 22 The duration from inf- to any point other than inf- is max+ and from inf+ to any point other than inf+ is max-. 
(forall (?t)
(and 	(if	  (and	(timepoint ?t)
			(not (= ?t inf-)))
		  (= max- (duration ?t inf-)))
	(if	  (and	(timepoint ?t)
			(not (= ?t inf+)))
		  (= max+ (duration ?t inf+)))))

Definitions 

(forall (?t1 ?t2 ?d)
(iff	(= ?t2 (time_add ?t1 ?d))
	(and	(timepoint ?t1)
		(timepoint ?t2)
		(timeduration ?d)
		(= ?d (duration ?t2 ?t1)))))