| Subject |
have domain3 |
have domain2 |
have domain1 |
be first domain of |
have range |
be second domain of |
documentation |
have axiom |
is an instance of |
|---|
| before | | TimePoint | TimePoint | valence | | subrelation | (before ?POINT1 ?POINT2) means that ?POINT1 precedes ?POINT2 on the universal timeline | (=>
(instance ?REL TransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(holds ?REL ?INST1 ?INST3))))
| TransitiveRelation |
| BeginFn | | | TimeInterval | rangeSubclass | TimePoint | inverse | A UnaryFunction that maps a TimeInterval to the TimePoint at which the interval begins | (equal (BeginFn (PastFn ?TIME)) NegativeInfinity)
| UnaryFunction |
| cooccur | | Physical | Physical | valence | | subrelation | (cooccur ?THING1 ?THING2) means that the Object or Process ?THING1 occurs at the same time as, together with, or jointly with the Object or Process ?THING2. This covers the following temporal relations: is co-incident with, is concurrent with, is contemporaneous with, and is concomitant with | (<=>
(cooccur ?PHYS1 ?PHYS2)
(equal (WhenFn ?PHYS1) (WhenFn ?PHYS2)))
| TemporalRelation |
| DayFn | | Month | PositiveInteger | identityElement | Day | distributes | A BinaryFunction that maps a number and a Month to the corresponding Day of the Month. For example, (DayFn 18 (MonthFn 8 (YearFn 1912))) denotes the 18th day of August 1912 | (=>
(instance (DayFn ?NUMBER ?MONTH) Day)
(lessThanOrEqualTo ?NUMBER 31))
| TemporalRelation |
| during | | TimeInterval | TimeInterval | valence | | subrelation | (during ?INTERVAL1 ?INTERVAL2) means that ?INTERVAL1 starts after and ends before ?INTERVAL2 | (=>
(subProcess ?SUBPROC ?PROC)
(or
(equal (WhenFn ?SUBPROC) (WhenFn ?PROC))
(during (WhenFn ?SUBPROC) (WhenFn ?PROC))))
| TransitiveRelation |
| earlier | | TimeInterval | TimeInterval | valence | | subrelation | (earlier INTERVAL1 INTERVAL2) means that INTERVAL1 ends before INTERVAL2 begins | (=>
(earlier ?INTERVAL1 ?INTERVAL2)
(before (EndFn ?INTERVAL1) (BeginFn ?INTERVAL2)))
| TransitiveRelation |
| EndFn | | | TimeInterval | rangeSubclass | TimePoint | inverse | A UnaryFunction that maps a TimeInterval to the TimePoint at which the interval ends | (equal (EndFn (FutureFn ?TIME)) PositiveInfinity)
| UnaryFunction |
| existant | | TimePosition | Physical | valence | | subrelation | This relation holds between an instance of Physical and an instance of TimePosition just in case the temporal lifespan of the former includes the latter. The constants located and existant are the basic spatial and temporal predicates, respectively | (=>
(result ?PROC ?OBJ)
(forall (?TIME)
(=>
(before ?TIME (BeginFn (WhenFn ?PROC)))
(not
(existant ?OBJ ?TIME)))))
| TemporalRelation |
| finishes | | TimeInterval | TimeInterval | valence | | subrelation | (finishes ?INTERVAL1 ?INTERVAL2) means that ?INTERVAL1 and ?INTERVAL2 are both TimeIntervals that have the same ending TimePoint and that ?INTERVAL2 begins before ?INTERVAL1 | (=>
(instance ?REL TransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(holds ?REL ?INST1 ?INST3))))
| TransitiveRelation |
| FutureFn | | | TimePosition | rangeSubclass | TimeInterval | inverse | A UnaryFunction that maps a TimePosition to the TimeInterval which it meets and which ends at PositiveInfinity | (starts (ImmediateFutureFn (WhenFn ?THING)) (FutureFn (WhenFn ?THING)))
| UnaryFunction |
| HourFn | | Day | PositiveRealNumber | identityElement | Hour | distributes | A BinaryFunction that maps a number and a Day to the corresponding Hour of the Day. For example, (HourFn 14 (DayFn 18 (MonthFn 8 (YearFn 1912)))) denotes the 14th hour, i.e. 2 PM, on the 18th day of August 1912 | (=>
(instance (HourFn ?NUMBER ?DAY) Hour)
(lessThan ?NUMBER 24))
| TemporalRelation |
| HourIntervalFn | | PositiveRealNumber | PositiveRealNumber | identityElement | TimeInterval | distributes | A BinaryFunction that maps two numbers to the Class of TimeIntervals that begin at the hour corresponding to the first number and that end at the hour corresponding to the second number. For example, (HourIntervalFn 6 12) returns the set of TimeIntervals that begin at 6 AM every day and that end at 12 noon every day. If necessary, we will define other interval functions for seconds, minutes, days, and/or months | (=>
(instance ?INTERVAL (HourIntervalFn ?NUMBER1 ?NUMBER2))
(and
(lessThan ?NUMBER1 24)
(lessThan ?NUMBER2 24)
(lessThan ?NUMBER1 ?NUMBER2)))
| TemporalRelation |
| ImmediateFutureFn | | | TimePosition | rangeSubclass | TimeInterval | inverse | A UnaryFunction that maps a TimePosition to a short, indeterminate TimeInterval that immediately follows the TimePosition | (starts (ImmediateFutureFn (WhenFn ?THING)) (FutureFn (WhenFn ?THING)))
| UnaryFunction |
| ImmediatePastFn | | | TimePosition | rangeSubclass | TimeInterval | inverse | A UnaryFunction that maps a TimePosition to a short, indeterminate TimeInterval that immediately precedes the TimePosition | (finishes (ImmediatePastFn (WhenFn ?THING)) (PastFn (WhenFn ?THING)))
| UnaryFunction |
| meetsTemporally | | TimeInterval | TimeInterval | valence | | subrelation | (meetsTemporally ?INTERVAL1 ?INTERVAL2) means that the terminal point of the TimeInterval ?INTERVAL1 is the initial point of the TimeInterval ?INTERVAL2 | (=>
(instance ?REL IntransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(not
(holds ?REL ?INST1 ?INST3)))))
| TemporalRelation |
| MinuteFn | | Hour | PositiveRealNumber | identityElement | Minute | distributes | A BinaryFunction that maps a number and an Hour to the corresponding Minute of the Hour. For example, (MinuteFn 15 (HourFn 14 (DayFn 18 (MonthFn 8 (YearFn 1912))))) denotes 15 minutes after 2 PM on the 18th day of August 1912 | (=>
(instance (MinuteFn ?NUMBER ?HOUR) Minute)
(lessThan ?NUMBER 60))
| TemporalRelation |
| MonthFn | | Year | PositiveInteger | identityElement | Month | distributes | A BinaryFunction that maps a number and a Year to the corresponding Month of the Year. For example (MonthFn 8 (YearFn 1912)) denotes the eighth Month, i.e. August, of the Year 1912 | (=>
(instance (MonthFn ?NUMBER ?YEAR) Month)
(lessThanOrEqualTo ?NUMBER 12))
| TemporalRelation |
| overlapsTemporally | | TimeInterval | TimeInterval | valence | | subrelation | (overlapsTemporally ?INTERVAL1 ?INTERVAL2) means that the two TimeIntervals ?INTERVAL1 and ?INTERVAL2 have a TimeInterval in common. Note that this is consistent with ?INTERVAL1 and ?INTERVAL2 being the same TimeInterval | (=>
(and
(time ?PHYS ?TIME1)
(time ?PHYS ?TIME2))
(or
(overlapsTemporally ?TIME1 ?TIME2)
(temporalPart ?TIME1 ?TIME2)
(temporalPart ?TIME2 ?TIME1)))
| TemporalRelation |
| PastFn | | | TimePosition | rangeSubclass | TimeInterval | inverse | A UnaryFunction that maps a TimePosition to the TimeInterval that meets it and that begins at NegativeInfinity | (meetsTemporally (PastFn (WhenFn ?THING)) (WhenFn ?THING))
| UnaryFunction |
| SecondFn | | Minute | PositiveRealNumber | identityElement | Second | distributes | A BinaryFunction that maps a number and a Minute to the corresponding Second of the Minute. For example, (SecondFn 9 (MinuteFn 15 (HourFn 14 (DayFn 18 (MonthFn 8 (YearFn 1912)))))) denotes 9 seconds and 15 minutes after 2 PM on the 18th day of August 1912 | (=>
(instance (SecondFn ?NUMBER ?MINUTE) Second)
(lessThan ?NUMBER 60))
| TemporalRelation |
| starts | | TimeInterval | TimeInterval | valence | | subrelation | (starts ?INTERVAL1 ?INTERVAL2) means that ?INTERVAL1 and ?INTERVAL2 are both TimeIntervals that have the same initial TimePoint and that ?INTERVAL1 ends before ?INTERVAL2 | (=>
(instance ?REL TransitiveRelation)
(forall (?INST1 ?INST2 ?INST3)
(=>
(and
(holds ?REL ?INST1 ?INST2)
(holds ?REL ?INST2 ?INST3))
(holds ?REL ?INST1 ?INST3))))
| TransitiveRelation |
| temporallyBetween | TimePoint | TimePoint | TimePoint | singleValued | | subrelation | (temporallyBetween ?POINT1 ?POINT2 ?POINT3) means that the TimePoint ?POINT2 is between the TimePoints ?POINT1 and ?POINT3, i.e. ?POINT1 is before ?POINT2 and ?POINT2 is before ?POINT3 | (=>
(and
(instance ?POINT TimePoint)
(not (equal ?POINT NegativeInfinity)))
(exists (?OTHERPOINT)
(temporallyBetween NegativeInfinity ?OTHERPOINT ?POINT)))
| TernaryPredicate |
| temporallyBetweenOrEqual | TimePoint | TimePoint | TimePoint | singleValued | | subrelation | (temporallyBetweenOrEqual ?POINT1 ?POINT2 ?POINT3) means that the TimePoint ?POINT1 is before or equal to the TimePoint ?POINT2 and ?POINT2 is before or equal to the TimePoint ?POINT3 | (<=>
(temporallyBetweenOrEqual ?POINT1 ?POINT2 ?POINT3)
(and
(beforeEq ?POINT1 ?POINT2)
(beforeEq ?POINT2 ?POINT3)))
| TernaryPredicate |
| time | | TimePosition | Physical | valence | | subrelation | A very general TemporalRelation that specifies, at any level of resolution, the TimePosition at which a particular Object or Process exists or occurs | (=>
(and
(time ?PHYS ?TIME1)
(time ?PHYS ?TIME2))
(or
(overlapsTemporally ?TIME1 ?TIME2)
(temporalPart ?TIME1 ?TIME2)
(temporalPart ?TIME2 ?TIME1)))
| TemporalRelation |
| WhenFn | | | Physical | rangeSubclass | TimeInterval | inverse | A UnaryFunction that maps an Object or Process to the exact TimeInterval during which it exists. Note that, for every TimePoint ?TIME outside of the TimeInterval (WhenFn ?THING), ?THING is not existant at ?TIME | (starts (ImmediateFutureFn (WhenFn ?THING)) (FutureFn (WhenFn ?THING)))
| UnaryFunction |
| YearFn | | | Integer | rangeSubclass | Year | inverse | A UnaryFunction that maps a number to the corresponding calendar Year. For example, (YearFn 1912) denotes the Year 1912 | (=>
(instance ?FUNCTION UnaryFunction)
(valence ?FUNCTION 1))
| UnaryFunction |
SUMO View all facts Glossary Help
