;; ;; PSL Core ;; ;;

;; PSL Core ;;

;;

;; Extension Name: psl_core.th

;; Primitive Lexicon:

;; Relations: ;;

(object ?x) ;;
(activity ?a) ;;
(activity_occurrence ?occ) ;;
(timepoint ?t) ;;
(before ?t1 ?t2) ;;
(occurrence_of ?occ ?a) ;;
(participates_in ?x ?occ ?t) ;;

;; Functions: ;;

(beginof ?occ) ;;
(endof ?occ) ;;

;; Constants: ;;

inf+ ;;
inf- ;;

;; Defined Lexicon:

;; Relations: ;;

(between ?t1 ?t2 ?t3) ;;
(beforeEq ?t1 ?t2) ;;
(betweenEq ?t1 ?t2 ?t3) ;;
(exists_at ?x ?t) ;;
(is_occurring_at ?occ ?t) ;;

;; Theories Required by this Extension: None

;; Definitional Extensions Required by this Extension: None ;;

;;

Axioms

;; Axiom 1 The before relation only holds between timepoints. ;;

(forall (?t1 ?t2)
	(=>	(before ?t1 ?t2)
		(and 	(timepoint ?t1) 
			(timepoint ?t2))))
  ;;

;; Axiom 2 The before relation is a total ordering. ;;

(forall (?t1 ?t2)
	(=>	(and 	(timepoint ?t1) 
			(timepoint ?t2))
		(or 	(= ?t1 ?t2) 
			(before ?t1 ?t2) 
			(before ?t2 ?t1))))
  ;;

;; Axiom 3 The before relation is irreflexive. ;;

(forall (?t1)
	(not (before ?t1 ?t1)))
  ;;

;; Axiom 4 The before relation is transitive. ;;

(forall (?t1 ?t2 ?t3)
	(=>	(and 	(before ?t1 ?t2) 
			(before ?t2 ?t3))
		(before ?t1 ?t3)))
  ;;

;; Axiom 5 The timepoint inf- is before all other timepoints. ;;

(forall (?t)
        (=>	(and 	(timepoint ?t) 
			(not (= ?t inf-)))
		(before inf- ?t)))
  ;;

;; Axiom 6 Every other timepoint is before inf+. ;;

(forall (?t)
        (=>	(and 	(timepoint ?t) 
			(not (= ?t inf+)))
		(before ?t inf+)))
  ;;

;; Axiom 7 Given any timepoint t other than inf-, there is a timepoint between ;; inf- and t. ;;

(forall (?t)
	(=>	(and 	(timepoint ?t) 
			(not (= ?t inf-)))
		(exists (?u) 
			(between inf- ?u ?t))))
  ;;

;; Axiom 8 Given any timepoint t other than inf+, there is a timepoint between ;; t and inf+. ;;

(forall (?t)
	(=>	(and 	(timepoint ?t) 
			(not (= ?t inf+)))
		(exists (?u) 
			(between ?t ?u inf+))))
  ;;

;; Axiom 9 Everything is either an activity, activity occurrence, timepoint, ;; or object. ;;

(forall (?x)
	(or 	(activity ?x) 
		(activity_occurrence ?x) 
		(timepoint ?x) 
		(object ?x)))
  ;;

;; Axiom 10 Objects, activities, activity occurrences, and timepoints are all ;; distinct kinds of things. ;;

(forall (?x)
(and (=> (activity ?x)
         (not (or (activity_occurrence ?x) (object ?x) (timepoint ?x))))
     (=> (activity_occurrence ?x)
         (not (or (object ?x) (timepoint ?x))))
     (=> (object ?x)
         (not (timepoint ?x)))))
  ;;

;; Axiom 11 The occurrence relation only holds between activities and ;; activity occurrences. ;;

(forall (?a ?occ)
	(=>	(occurrence_of ?occ ?a)
		(and	(activity ?a)
			(activity_occurrence ?occ))))
  ;;

;; Axiom 12 Every activity occurrence is the occurrence of some activity. ;;

(forall (?occ)
	(=>	(activity_occurrence ?occ)
		(exists (?a)
			(and	(activity ?a)
				(occurrence_of ?occ ?a)))))
  ;;

;; Axiom 13 An activity occurrence is associated with a unique activity. ;;

(forall (?occ ?a1 ?a2)
        (=>	(and	(occurrence_of ?occ ?a1)
                        (occurrence_of ?occ ?a2))
		(= ?a1 ?a2)))
  ;;

;; Axiom 14 The begin and end of an activity occurrence or object are timepoints. ;; ;;

(forall (?a ?x)
	(=>	(or	(occurrence_of ?x ?a)
			(object ?x))
		(and 	(timepoint (beginof ?x))
         		(timepoint (endof ?x)))))
  ;;

;; Axiom 15 The begin point of every activity occurrence or object is ;; before or equal to its end point. ;;

(forall (?x)
	(=>	(or	(activity_occurrence ?x)
			(object ?x))
		(beforeEq (beginof ?x) (endof ?x))))
  ;;

;; Axiom 16 The participates_in relation only holds between objects, ;; activity occurrences, and timepoints, respectively. ;;

(forall (?x ?occ ?t)
	(=>	(participates_in ?x ?occ ?t)
		(and 	(object ?x) 
			(activity_occurrence ?occ) 
			(timepoint ?t))))
  ;;

;; Axiom 17 An object can participate in an activity occurrence only at those timepoints ;; at which both the object exists and the activity is occurring. ;;

(forall (?x ?occ ?t)
	(=>	(participates_in ?x ?occ ?t)
		(and 	(exists_at ?x ?t)
         		(is_occurring_at ?occ ?t))))
  ;;

;;

Supporting Definitions

;; Definition 1 Timepoint ?t2 is between timepoints ?t1 and ?t3 if and only if ?t1 is before ;; ?t2 and ?t2 is before ?t3. ;;

(forall (?t1 ?t2 ?t3) (<=> (between ?t1 ?t2 ?t3)
  (and (before ?t1 ?t2) (before ?t2 ?t3))))
  ;;

;; Definition 2 Timepoint ?t1 is beforeEq timepoint ?t2 if and only if ?t1 is before or equal ;; to ?t2. ;;

(forall (?t1 ?t2) (<=> (beforeEq ?t1 ?t2)
  (and (timepoint ?t1) (timepoint ?t2)
       (or (before ?t1 ?t2) (= ?t1 ?t2)))))
  ;;

;; Definition 3 Timepoint ?t2 is betweenEq timepoints ?t1 and ?t3 if and only if ;; ?t1 is before or equal to ?t2, and ?t2 is before or equal to ?t3. ;;

(forall (?t1 ?t2 ?t3) (<=> (betweenEq ?t1 ?t2 ?t3)
  (and (beforeEq ?t1 ?t2)
       (beforeEq ?t2 ?t3))))
  ;;

;; Definition 4 An object exists at a timepoint ?t if and only if ?t is betweenEq its begin ;; and end points. ;;

(forall (?x ?t) (<=> (exists_at ?x ?t)
  (and (object ?x)
       (betweenEq (beginof ?x) ?t (endof ?x)))))
  ;;

;; Definition 5 An activity is occurring at a timepoint ?t if and only if ?t ;; is betweenEq the begin and end points activity occurrence. ;;

(forall (?occ ?t) (<=> (is_occurring_at ?occ ?t)
	(betweenEq (beginof ?occ) ?t (endof ?occ))))
  ;;

;;