(define-theory Unrestricted-Time (Mereology Top-Level))

(in-theory 'Unrestricted-Time)


(DEFINE-RELATION ANTEDATES (?A ?B)
 "Two entities whatsoever existing in disjoint time-spans. 
This is useful for temporal precedence involving non-temporalized entities."
 :DEF
 (AND (EXISTS (?Z ?W)
       (AND (TIME-SPAN ?Z)
            (TIME-SPAN ?W)
            (TEMPORALLY-CONTAINS ?Z ?A)
            (TEMPORALLY-CONTAINS ?W ?B)
            (PRECEDES ?Z ?W)))
      (TEMPORAL-RELATION ?A ?B)
      (ENTITY ?A)
      (ENTITY ?B))
 :CONSTRAINTS (AND (ENTITY ?A) (ENTITY ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE ANTEDATES ENTITY)
      (DOMAIN ANTEDATES ENTITY)))
(DEFINE-FUNCTION BEGINPOINT (?A) :-> ?B
 "A beginpoint of a process is its initial pointillistic 
part. The use of 'meets' in the definition requires a mereologic definition of meets, 
otherwise beginpoint and meets are circularly introduced."
 :DEF
 (AND (TEMPORAL-PART-OF ?B ?A)
      (NOT (EXISTS ?Z (AND (TEMPORAL-PART-OF ?Z ?A) (MEETS ?Z ?B))))
      (TIME-FUNCTION ?A ?B))
 :AXIOM-DEF (FUNCTION BEGINPOINT) :AXIOM-CONSTRAINTS
 (AND (RANGE BEGINPOINT TEMPORALIZED-ENTITY)
      (DOMAIN BEGINPOINT TEMPORALIZED-ENTITY)))
(DEFINE-RELATION CO-EXIST (?A ?B)
 "Two entities whatsoever within the same time-span. Here there is 
also a localization restriction, useful to accomplish a relevance criterion usually implicit
in coexistence (specially in biomedicine). This is useful for 'co-occurrence' involving 
non-temporalized entities."
 :DEF
 (AND (EXISTS ?Z
       (AND (TIME-SPAN ?Z)
            (TEMPORALLY-CONTAINS ?Z ?A)
            (TEMPORALLY-CONTAINS ?Z ?B)
            (EXISTS ?W
             (AND (REGION ?W) (LOCATED ?W ?A) (LOCATED ?W ?B)))))
      (TEMPORAL-RELATION ?A ?B)))
(DEFINE-RELATION CO-OCCUR (?A ?B)
 "Occurs at the same time as, together with, or jointly.  
This includes is co-incident with, is concurrent with, is contemporaneous with, 
and is concomitant with. Diagrammatically: =; if absolute time is not wanted in the 
definition, co-occur can be taken as a non-axiomatized primitive."
 :DEF
 (AND (EXISTS ?U
       (AND (EXISTS (?C ?D ?E ?F)
             (AND (BEGINPOINT ?B ?F)
                  (TIME-VALUE ?F ?E)
                  (BEGINPOINT ?A ?D)
                  (TIME-VALUE ?D ?C)
                  (= ?C ?E)))
            (EXISTS (?G ?H ?I ?J)
             (AND (ENDPOINT ?B ?J)
                  (TIME-VALUE ?J ?I)
                  (ENDPOINT ?A ?H)
                  (TIME-VALUE ?H ?G)
                  (= ?G ?I)))
            (EXISTS (?K) (AND (THE-TIME-UNIT ?A ?K) (IDENTITY ?K ?U)))
            (EXISTS (?L) (AND (THE-TIME-UNIT ?B ?L) (IDENTITY ?L ?U)))))
      (TEMPORAL-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE CO-OCCUR TEMPORALIZED-ENTITY)
      (DOMAIN CO-OCCUR TEMPORALIZED-ENTITY)))
(DEFINE-RELATION DEPENDENTLY-ANTEDATES (?A ?B)
 "Two entities whatsoever existing in disjoint time-spans,
and the second depends on the first."
 :IFF-DEF (AND (ANTEDATES ?A ?B) (STRICTLY-NECESSARY-TO ?A ?B)))
(DEFINE-RELATION DEPENDENTLY-CO-EXIST (?A ?B)
 "Two entities whatsoever existing in the same time-span,
and symmetrical depending one another."
 :IFF-DEF
 (AND (CO-EXIST ?A ?B)
      (STRICTLY-NECESSARY-TO ?A ?B)
      (STRICTLY-DEPENDS-ON ?A ?B)))
(DEFINE-RELATION DEPENDENTLY-POSTDATES (?A ?B) :IFF-DEF
 (AND (NOT (IDENTITY ?A ?B))
      (STRICTLY-DEPENDS-ON ?A ?B)
      (POSTDATES ?A ?B)
      (ENTITY ?A)
      (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE DEPENDENTLY-POSTDATES ENTITY)
      (DOMAIN DEPENDENTLY-POSTDATES ENTITY)))
(define-class present (?a))
(DEFINE-FUNCTION DURATION-VALUE (?A) :-> ?B
 "The value of a duration, without a specified time line.
We also support an existence assumption: an entity has existence only during its duration
value."
 :DEF
 (AND (EXISTS (?Z ?T)
       (AND (PRESENT ?T)
            (TIME-SPAN ?Z)
            (BEGINS-AT ?T ?Z)
            (EXISTS (?C) (AND (DURATION-VALUE ?Z ?C) (IDENTITY ?C ?B)))
            (BEGINS-AT ?T "(HAS-EXISTENCE ?A TRUE)")
            (FORALL (?W ?T1)
             (=>
              (AND (PRESENT ?T1)
                   (/= ?T ?T1)
                   (TIME-SPAN ?W)
                   (BEGINS-AT ?T1 ?W)
                   (OR (PRECEDES ?W ?Z) (FOLLOWS ?W ?Z)))
              (EXISTS (?E)
               (AND (NOT (HAS-EXISTENCE ?A TRUE)) (BEGINS-AT ?T1 ?E)))))))
      (EXISTS ?U
       (AND (TIME-UNIT ?U)
            (EXISTS (?F) (AND (THE-TIME-UNIT ?A ?F) (IDENTITY ?F ?U)))))
      (NUMERIC-VALUE ?A ?B))
 :AXIOM-DEF (FUNCTION DURATION-VALUE) :AXIOM-CONSTRAINTS
 (RANGE DURATION-VALUE NUMBER))
(DEFINE-RELATION DURING (?A ?B) "Contained in some temporal entity."
 :DEF
 (AND (EXISTS (?C ?D)
       (AND (BEGINPOINT ?A ?D) (BEGINPOINT ?B ?C) (PRECEDES ?C ?D)))
      (EXISTS (?E ?F)
       (AND (ENDPOINT ?B ?F) (ENDPOINT ?A ?E) (PRECEDES ?E ?F)))
      (TEMPORAL-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE DURING TEMPORALIZED-ENTITY)
      (DOMAIN DURING TEMPORALIZED-ENTITY)))
(DEFINE-FUNCTION ENDPOINT (?A) :-> ?B
 "An endpoint of a process is its final pointillistic 
part. The use of 'meets' in the definition requires a mereologic definition of meets, 
otherwise endpoint and meets are circularly introduced. The only other possibility is
having meets as non-axiomatized primitive."
 :DEF
 (AND (TEMPORAL-PART-OF ?B ?A)
      (NOT (EXISTS ?Z (AND (TEMPORAL-PART-OF ?Z ?A) (MEETS ?B ?Z))))
      (TIME-FUNCTION ?A ?B))
 :AXIOM-DEF (FUNCTION ENDPOINT) :AXIOM-CONSTRAINTS
 (AND (RANGE ENDPOINT TEMPORALIZED-ENTITY)
      (DOMAIN ENDPOINT TEMPORALIZED-ENTITY)))
(DEFINE-RELATION FINISHED-BY (?A ?B) :IFF-DEF
 (= (INVERSE FINISHES) FINISHED-BY))
(DEFINE-RELATION FINISHES (?A ?B)
 "Same ending point, different beginning point." :DEF
 (AND (EXISTS (?C ?D)
       (AND (ENDPOINT ?B ?D) (ENDPOINT ?A ?C) (CO-OCCUR ?C ?D)))
      (NOT (EXISTS (?E ?F)
            (AND (BEGINPOINT ?B ?F) (BEGINPOINT ?A ?E) (CO-OCCUR ?E ?F))))
      (TEMPORAL-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE FINISHES TEMPORALIZED-ENTITY)
      (DOMAIN FINISHES TEMPORALIZED-ENTITY)))
(DEFINE-RELATION FOLLOWS (?A ?B) :IFF-DEF
 (AND (= (INVERSE PRECEDES) FOLLOWS) (ENTITY ?A) (ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE FOLLOWS ENTITY)
      (DOMAIN FOLLOWS ENTITY)))
(DEFINE-RELATION IS-BEGINPOINT-OF (?A ?B) :IFF-DEF
 (= (INVERSE BEGINPOINT) IS-BEGINPOINT-OF))
(DEFINE-RELATION IS-DURATION-VALUE-OF (?A ?B) :IFF-DEF
 (AND (= (INVERSE DURATION-VALUE) IS-DURATION-VALUE-OF)
      (NUMBER ?A))
 :AXIOM-CONSTRAINTS
 (DOMAIN IS-DURATION-VALUE-OF NUMBER))
(DEFINE-RELATION IS-ENDPOINT-OF (?A ?B) :IFF-DEF
 (= (INVERSE ENDPOINT) IS-ENDPOINT-OF))
(DEFINE-RELATION IS-TIME-VALUE-OF (?A ?B) :IFF-DEF
 (= (INVERSE TIME-VALUE) IS-TIME-VALUE-OF))
(DEFINE-RELATION MEETS (?A ?B)
 "Temporal connection; diagrammatically: --." :DEF
 (AND (NOT (EXISTS ?Z
            (AND (TIME-SPAN ?Z) (PRECEDES ?Z ?B) (PRECEDES ?A ?Z))))
      (TEMPORAL-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE MEETS TEMPORALIZED-ENTITY)
      (DOMAIN MEETS TEMPORALIZED-ENTITY)))
(DEFINE-RELATION MET-BY (?A ?B) :IFF-DEF (= (INVERSE MEETS) MET-BY))
(DEFINE-RELATION POSTDATES (?A ?B) :IFF-DEF
 (AND (= (INVERSE ANTEDATES) POSTDATES) (ENTITY ?A) (ENTITY ?B)) :CONSTRAINTS
 (AND (ENTITY ?A) (ENTITY ?B)) :AXIOM-CONSTRAINTS
 (AND (RANGE POSTDATES ENTITY)
      (DOMAIN POSTDATES ENTITY)))
(DEFINE-RELATION PRECEDES (?A ?B)
 "Diagrammatically: - -; if absolute time is not wanted in the 
definition, precedes can be taken as a primitive.
To take into account platformed processes, we should also introduce different time-spans 
which contextualize branching platforms."
 :DEF
 (AND (EXISTS ?U
       (AND (EXISTS (?C ?D ?E ?F)
             (AND (BEGINPOINT ?B ?F)
                  (DURATION-VALUE ?F ?E)
                  (ENDPOINT ?A ?D)
                  (TIME-VALUE ?D ?C)
                  (< ?C ?E)))
            (EXISTS (?G) (AND (THE-TIME-UNIT ?A ?G) (IDENTITY ?G ?U)))
            (EXISTS (?H) (AND (THE-TIME-UNIT ?B ?H) (IDENTITY ?H ?U)))))
      (TEMPORAL-RELATION ?A ?B)
      (ENTITY ?A)
      (ENTITY ?B))
 :CONSTRAINTS (AND (TEMPORALIZED-ENTITY ?A) (TEMPORALIZED-ENTITY ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE PRECEDES ENTITY)
      (DOMAIN PRECEDES ENTITY)))
(DEFINE-RELATION STARTED-BY (?A ?B) :IFF-DEF
 (= (INVERSE STARTS) STARTED-BY))
(DEFINE-RELATION STARTS (?A ?B)
 "Same beginning point, different ending point." :DEF
 (AND (EXISTS (?C ?D)
       (AND (BEGINPOINT ?B ?D) (BEGINPOINT ?A ?C) (CO-OCCUR ?C ?D)))
      (NOT (EXISTS (?E ?F)
            (AND (ENDPOINT ?B ?F) (ENDPOINT ?A ?E) (CO-OCCUR ?E ?F))))
      (TEMPORAL-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE STARTS TEMPORALIZED-ENTITY)
      (DOMAIN STARTS TEMPORALIZED-ENTITY)))
(DEFINE-RELATION T-OVERLAPS (?A ?B)
 "Sharing of a temporal part; two alternatives: 
x t-overlaps & partly precedes y, or x t-overlaps and partly follows y."
 :DEF
 (AND (OR (AND (EXISTS (?C ?D)
                (AND (BEGINPOINT ?B ?D) (BEGINPOINT ?A ?C) (PRECEDES ?C ?D)))
               (EXISTS (?E ?F)
                (AND (ENDPOINT ?B ?F) (ENDPOINT ?A ?E) (PRECEDES ?E ?F))))
          (AND (EXISTS (?G ?H)
                (AND (BEGINPOINT ?A ?H) (BEGINPOINT ?B ?G) (PRECEDES ?G ?H)))
               (EXISTS (?I ?J)
                (AND (ENDPOINT ?A ?J) (ENDPOINT ?B ?I) (PRECEDES ?I ?J)))))
      (TEMPORAL-RELATION ?A ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE T-OVERLAPS TEMPORALIZED-ENTITY)
      (DOMAIN T-OVERLAPS TEMPORALIZED-ENTITY)))
(DEFINE-RELATION TEMPORALLY-CONTAINS (?A ?B) :IFF-DEF
 (= (INVERSE DURING) TEMPORALLY-CONTAINS))
(DEFINE-FUNCTION TIME-VALUE (?A) :-> ?B
 "The value of a time point, with a specified 
time line (the time of happening, absolute)."
 :DEF
 (AND (EXISTS ?U
       (AND (TIME-UNIT ?U)
            (EXISTS (?C) (AND (THE-TIME-UNIT ?A ?C) (IDENTITY ?C ?U)))))
      (VALUE ?A ?B))
 :AXIOM-DEF (FUNCTION TIME-VALUE) :AXIOM-CONSTRAINTS
 (RANGE TIME-VALUE VALUE-FILLER))
(DEFINE-RELATION _CYCLIC (?A ?B))
(DEFINE-RELATION _INTERMITTENT (?A ?B))
(DEFINE-RELATION _POINTILLISTIC (?A ?B))
(DEFINE-RELATION _RANDOM-INTERMITTENT (?A ?B))
(DEFINE-CLASS DATE-VALUE-FILLER (?SELF)
:DEF (VALUE-FILLER ?SELF))
(DEFINE-CLASS PLATFORM (?SELF)
 "A platform allows the contextualization of diverging processes 
within the same narrative."
 :DEF
 (AND (TEMPORALIZED-ENTITY ?SELF)
      (EXISTS (?A)
              (AND (TEMPORALLY-CONTAINS ?SELF ?A)
                   (AND (ACTIVITY ?A)
                        (EXISTS (?B)
                                (AND (REPRESENTED-BY ?A ?B) (NARRATIVE ?B))))))
      (EXISTS (?C) (AND (DURING ?SELF ?C) (TIME-SPAN ?C)))))