Skip to content
Permalink
Browse files

new hierarchies, theories, and theorems related to SUMO temporal conc…

…epts
  • Loading branch information...
gruninger committed Mar 8, 2016
1 parent ce264eb commit a2e7e54d90c2b21ac6dbd9cc6bb9197aa96a930a
Showing with 2,151 additions and 0 deletions.
  1. +259 −0 ontologies/sumo/sumo_temporalPart
  2. +343 −0 ontologies/sumo/sumo_time.clif
  3. +89 −0 ontologies/sumo/sumo_timepoints
  4. +85 −0 ontologies/sumo/theorems/input/sumo_time.in
  5. +30 −0 ontologies/sumo/theorems/output/ex128-1.in
  6. +55 −0 ontologies/sumo/theorems/output/ex128-1.model
  7. +27 −0 ontologies/sumo/theorems/output/ex128-2.in
  8. +49 −0 ontologies/sumo/theorems/output/ex128-2.model
  9. +52 −0 ontologies/sumo/theorems/output/ex128-3.in
  10. +275 −0 ontologies/sumo/theorems/output/ex128-3.model
  11. +39 −0 ontologies/sumo/theorems/timepoints_entails/ex129-1.in
  12. +35 −0 ontologies/sumo/theorems/timepoints_entails/ex129-1.proof
  13. +38 −0 ontologies/sumo/theorems/timepoints_entails/ex129-10.in
  14. +43 −0 ontologies/sumo/theorems/timepoints_entails/ex129-10.proof
  15. +39 −0 ontologies/sumo/theorems/timepoints_entails/ex129-2.in
  16. +26 −0 ontologies/sumo/theorems/timepoints_entails/ex129-2.proof
  17. +39 −0 ontologies/sumo/theorems/timepoints_entails/ex129-3.in
  18. +39 −0 ontologies/sumo/theorems/timepoints_entails/ex129-3.proof
  19. +38 −0 ontologies/sumo/theorems/timepoints_entails/ex129-4.in
  20. +43 −0 ontologies/sumo/theorems/timepoints_entails/ex129-4.proof
  21. +38 −0 ontologies/sumo/theorems/timepoints_entails/ex129-5.in
  22. +28 −0 ontologies/sumo/theorems/timepoints_entails/ex129-5.proof
  23. +38 −0 ontologies/sumo/theorems/timepoints_entails/ex129-6.in
  24. +35 −0 ontologies/sumo/theorems/timepoints_entails/ex129-6.proof
  25. +38 −0 ontologies/sumo/theorems/timepoints_entails/ex129-7.in
  26. +35 −0 ontologies/sumo/theorems/timepoints_entails/ex129-7.proof
  27. +38 −0 ontologies/sumo/theorems/timepoints_entails/ex129-8.in
  28. +33 −0 ontologies/sumo/theorems/timepoints_entails/ex129-8.proof
  29. +38 −0 ontologies/sumo/theorems/timepoints_entails/ex129-9.in
  30. +33 −0 ontologies/sumo/theorems/timepoints_entails/ex129-9.proof
  31. +33 −0 ontologies/sumo_timeintervals/mappings/delta.in
  32. +10 −0 ontologies/sumo_timeintervals/mappings/pi.in
  33. +56 −0 ontologies/sumo_timeintervals/sumo_timeintervals.clif
  34. +55 −0 ontologies/sumo_timepoints/sumo_ordered_timepoints.clif
@@ -0,0 +1,259 @@

(cl-text colore.oor.net/sumo/sumo_temporalPart

(forall (x y)
(if (and (temporalPart x y)
(temporalPart y x))
(= x y)))

(forall (x y z)
(if (and (temporalPart x y)
(temporalPart y z))
(temporalPart x z)))

(forall (x y)
(if (overlapsTemporally x y)
(and (TimeInterval x)
(TimeInterval y))))

(forall (x)
(if (TimeInterval x)
(overlapsTemporally x x)))

(forall (x y)
(if (overlapsTemporally x y)
(overlapsTemporally y x)))

(forall (x y)
(iff (overlapsTemporally x y)
(exists (z)
(and (TimeInterval z)
(temporalPart z x)
(temporalPart z y)))))

(forall (x y)
(if (starts x y)
(and (TimeInterval x)
(TimeInterval y))))

(forall (x y z)
(if (and (starts x y)
(starts y z))
(starts x z)))

(forall (x)
(if (TimeInterval x)
(not (starts x x))))

(forall (x y)
(if (starts x y)
(temporalPart x y)))

(forall (x y)
(iff (starts x y)
(and (TimeInterval x)
(TimeInterval y)
(before (EndFn x) (EndFn y))
(= (BeginFn x) (BeginFn y)))))

(forall (x y)
(if (finishes x y)
(and (TimeInterval x)
(TimeInterval y))))

(forall (x y z)
(if (and (finishes x y)
(finishes y z))
(finishes x z)))

(forall (x)
(if (TimeInterval x)
(not (finishes x x))))

(forall (x y)
(if (finishes x y)
(temporalPart x y)))

(forall (x y)
(iff (finishes x y)
(and (TimeInterval x)
(TimeInterval y)
(before (BeginFn x) (BeginFn y))
(= (EndFn x) (EndFn y)))))

(forall (x y)
(if (during x y)
(and (TimeInterval x)
(TimeInterval y))))

(forall (x y z)
(if (and (during x y)
(during y z))
(during x z)))

(forall (x)
(if (TimeInterval x)
(not (during x x))))

(forall (x y)
(if (during x y)
(temporalPart x y)))

(forall (x y)
(if (during x y)
(and (TimeInterval x)
(TimeInterval y)
(before (EndFn x) (EndFn y))
(before (BeginFn y) (BeginFn x)))))

(forall (x y)
(if (earlier x y)
(and (TimeInterval x)
(TimeInterval y))))

(forall (x y z)
(if (and (earlier x y)
(earlier y z))
(earlier x z)))

(forall (x)
(if (TimeInterval x)
(not (earlier x x))))

(forall (x y)
(iff (earlier x y)
(and (TimeInterval x)
(TimeInterval y)
(before (EndFn x) (BeginFn y)))))

(forall (x y)
(if (meetsTemporally x y)
(and (TimeInterval x)
(TimeInterval y))))

(forall (x y z)
(if (and (meetsTemporally x y)
(meetsTemporally y z))
(not (meetsTemporally x z))))

(forall (x y)
(if (meetsTemporally x y)
(not (meetsTemporally y x))))

(forall (x y)
(iff (meetTemporally x y)
(and (TimeInterval x)
(TimeInterval y)
(= (EndFn x) (BeginFn y)))))

(forall (x)
(TimeInterval x)
(temporalPart x x))

(forall (x)
(if (TimeInterval x)
(Timeposition x)))

(forall (x)
(if (TimePoint x)
(Timeposition x)))

(forall (x)
(if (TimePosition x)
(or (TimeInterval x)
(TimePoint x))))

(forall (x)
(if (TimeInterval x)
(not (TimePoint x))))

(forall (x y)
(if (temporalPart x y)
(and (TimePosition x)
(TimePosition y))))

(forall (x)
(if (TimePosition x)
(temporalPart x x)))

(forall (x)
(if (and (temporalPart x y)
(temporalPart y x))
(= x y)))

(forall (x y z)
(if (and (temporalPart x y)
(temporalPart y z))
(temporalPart x z)))

(forall (x)
(if (TimePoint x)
(exists (y)
(and (TimeInterval y)
(temporalPart x y)))))

(forall (x)
(if (TimeInterval x)
(exists (y)
(and (TimePoint y)
(temporalPart y x)))))

(forall (x y z t)
(if (and (TimePoint x)
(TimePoint y)
(TimeInterval z)
(= (TimeIntervalFn x y) z)
(TimePoint t))
(iff (temporallyBetweenOrEqual x t y)
(temporalPart t z))))

(forall (x y z)
(if (and (TimePoint x)
(TimePoint y)
(TimeInterval z)
(= (TimeIntervalFn x y) z))
(and (= (BeginFn z) x)
(= (EndFn z) y))))

(forall (x y z t)
(if (and (TimeInterval x)
(TimeInterval y)
(TimePoint z)
(TimePoint t)
(= (BeginFn x) z)
(= (BeginFn y) z)
(= (EndFn x) t)
(= (EndFn y) t))
(= x y)))

(forall (x y)
(if (and (TimeInterval x)
(TimePoint y)
(= (BeginFn x) y))
(forall (z)
(if (and (temporalPart z x)
(TimePoint z)
(not (= z y)))
(before y z)))))

(forall (x y)
(if (and (TimeInterval x)
(TimePoint y)
(= (EndFn x) y))
(forall (z)
(if (and (temporalPart z x)
(TimePoint z)
(not (= z y)))
(before z y)))))

(forall (z u v)
(if (and (TimeInterval z)
(TimePoint u)
(TimePoint v)
(= (BeginFn z) u)
(= (EndFn z) v))
(before u v)))



)
Oops, something went wrong.

0 comments on commit a2e7e54

Please sign in to comment.
You can’t perform that action at this time.