(cl:text "Date-Time Vocabulary"
(cl:comment '
moduleName: Date-Time Vocabulary
moduleAbbreviation: DTV
moduleVersion: 1.1
moduleAbstract: This file contains CLIF for portions of the Date-Time Vocabulary. See http://www.omg.org/spec/DTV.
filename: dtv.clif
documentNumber: dtc/2016-02-25
documentURL: http:/www.omg.org/spec/DTV/20160301/dtv.clif
isNormative: true
contentType: vocabulary
contentLanguage: http://standards.iso.org/ittf/PubliclyAvailableStandards/c039175_ISO_IEC_24707_2007%28E%29.zip
format: CLIF
directSource: http:/www.omg.org/cgi-bin/doc?dtc/2016-02-20
copyright: Copyright (c) 2015, Object Management Group
')
(cl:imports MinimalMereology)
(cl:imports Sequences)
(cl:imports Quantities)
(cl:comment 'Time interval2 is a component of time interval1. Every instant in time interval1 is also in time interval2. Everything that happens in time interval1 happens in time interval2')
(forall (t1 t2)
(if ("time interval1 is part of time interval2" t1 t2)
(and ("time interval" t1) ("time interval" t2)
("thing1 is part of thing2" t1 t2)) ))
(cl:comment 'time interval1 overlaps time interval2 ')
(forall (t1 t2)
(if ("time interval1 overlaps time interval2" t1 t2)
(and ("time interval" t1) ("time interval" t2)
("thing1 overlaps thing2" t1 t2))))
(cl:comment 'time interval1 is a proper part of time interval2 ')
(forall (t1 t2)
(if ("time interval1 is proper part of time interval2" t1 t2)
(and ("time interval" t1) ("time interval" t2)
("thing1 is proper part of thing2" t1 t2))))
(cl:comment 'For each time interval1, there is at least one time interval2 that is a proper part of time interval1.')
(forall (ti1 "time interval")
(exists (ti2 "time interval")
("proper part of" ti2 ti1) ))
(cl:comment 'time interval1 ends before/when time interval2 starts ')
(forall (t1 t2)
(if ("time interval1 is before time interval2" t1 t2)
(and ("time interval" t1) ("time interval" t2))))
(cl:comment 'If a time interval1 overlaps a time interval2, then the time interval1 is not before the time interval2.')
(forall (t1 t2)
(if ("time interval1 overlaps time interval2" t1 t2)
(and
(not ("time interval1 is before time interval2" t1 t2))
(not ("time interval1 is before time interval2" t2 t1)) )))
(cl:comment 'If a time interval1 does not overlap a time interval2, then the time interval1 is before the time interval2 or the time interval2 is before the time interval1.')
(forall ((t1 "time interval") (t2 "time interval"))
(if (not ("time interval1 overlaps time interval2" t1 t2))
(or ("time interval1 is before time interval2" t1 t2)
("time interval1 is before time interval2" t2 t1))))
(cl:comment 'A given time interval is not before the time interval.')
(forall ((t1 "time interval"))
(not ("time interval1 is before time interval2" t1 t1)))
(cl:comment 'If a time interval1 is before a time interval2, then the time interval2 is not before the time interval1.')
(forall (t1 t2)
(if ("time interval1 is before time interval2" t1 t2)
(not ("time interval1 is before time interval2" t2 t1))))
(cl:comment 'Each time interval1 overlaps each time interval2 and time interval1 is not before time interval2 and time interval2 is not before time interval1, or time interval1 is before time interval2 and time interval1 does not overlap time interval2 and time interval2 is not before time interval1, or time interval2 is before time interval1 and time interval1 does not overlap time interval2 and time interval1 is not before time interval2.')
(forall ((t1 "time interval") (t2 "time interval"))
(or
("time interval1 overlaps time interval2" t1 t2)
(and
("time interval1 is before time interval2" t1 t2)
(not ("time interval1 overlaps time interval2" t1 t2)))
(and
("time interval1 is before time interval2" t2 t1)
(not ("time interval1 overlaps time interval2" t1 t2)))
))
(cl:comment 'If a time interval1 is before a time interval2 and the time interval2 is before a time interval3 then the time interval1 is before the time interval3.')
(forall (t1 t2 t3)
(if
(and
("time interval1 is before time interval2" t1 t2)
("time interval1 is before time interval2" t2 t3))
("time interval1 is before time interval2" t1 t3)))
(cl:comment 'time interval1 is before time interval2 and some time interval3 is after time interval1 and is before time interval2')
(forall (t1 t2)
(iff ("time interval1 is properly before time interval2" t1 t2)
(and
("time interval" t1) ("time interval" t2)
("time interval1 is before time interval2" t1 t2)
(exists (t3)
(and ("time interval1 is before time interval2" t1 t3)
("time interval1 is before time interval2" t3 t2))
) )))
(cl:comment 'time interval1 equals time interval2
Definition: the time interval1 is part of the time interval2 and the time interval2 is part of the time interval1'
)
(forall (t1 t2)
(iff ("time interval1 equals time interval2" t1 t2)
(and ("time interval1 is part of time interval2" t1 t2)
("time interval1 is part of time interval2" t2 t1))
))
(cl:comment 'Necessity: A time interval1 equals a time interval2 if and only if time interval1 is time interval2' )
(forall (ti1 ti2)
(if (and ("time interval" ti1) ("time interval" ti2))
(iff ("time interval1 equals time interval2" ti1 ti2)
("thing1 is thing2" ti1 ti2) )))
(cl:comment 'time interval1 is before time interval2 and no time interval3 is after time interval1 and is before time interval2')
(forall (t1 t2)
(iff ("time interval1 meets time interval2" t1 t2)
(and
("time interval1 is before time interval2" t1 t2)
(not (exists (t3)
(and ("time interval1 is before time interval2" t1 t3)
("time interval1 is before time interval2" t3 t2))
)) )))
(cl:comment 'time interval1 overlaps time interval2 and some part of time interval1 is before time interval2')
(forall (t1 t2)
(iff ("time interval1 properly overlaps time interval2" t1 t2)
(and
("time interval1 overlaps time interval2" t1 t2)
(exists (t3)
(and ("time interval1 is proper part of time interval2" t3 t1)
("time interval1 is before time interval2" t3 t2))
) )))
(cl:comment 'time interval1 is part of time interval2 and some part of time interval2 is before time interval1 and some part of time interval2 is after time interval1')
(forall (t1 t2)
(iff ("time interval1 is properly during time interval2" t1 t2)
(and
("time interval1 is proper part of time interval2" t1 t2)
(not ("time interval1 starts time interval2" t1 t2))
(not ("time interval1 finishes time interval2" t1 t2))
)))
(cl:comment 'time interval1 is a proper part of time interval2 and no part of time interval2 is before time interval1')
(forall (t1 t2)
(iff ("time interval1 starts time interval2" t1 t2)
(and
("time interval1 is proper part of time interval2" t1 t2)
(not (exists (t3)
(and ("time interval1 is proper part of time interval2" t3 t2)
("time interval1 is before time interval2" t3 t1)) ))
)))
(cl:comment 'time interval1 is a proper part of time interval2 and no part of time interval2 is after time interval1')
(forall (t1 t2)
(iff ("time interval1 finishes time interval2" t1 t2)
(and
("time interval1 is proper part of time interval2" t1 t2)
(not (exists (t3)
(and ("time interval1 is proper part of time interval2" t3 t2)
("time interval1 is before time interval2" t1 t3)) ))
)))
(cl:comment 'time interval1 starts before time interval2
Definition: some time interval3 is part of time interval1 and is before time interval2 '
)
(forall (t1 t2)
(iff ("time interval1 starts before time interval2" t1 t2)
(exists (t3)
(and
("time interval1 is before time interval2" t3 t2)
("time interval1 is part of time interval2" t3 t1) ))))
(cl:comment 'time interval1 starts with time interval2
Definition: time interval1 starts time interval2 or time interval2 starts time interval1 or time interval1 equals time interval2 '
)
(forall (t1 t2)
(iff ("time interval1 starts with time interval2" t1 t2)
(or
("time interval1 starts time interval2" t1 t2)
("time interval1 starts time interval2" t2 t1)
("time interval1 equals time interval2" t1 t2)) ))
(cl:comment 'Necessity: If time interval1 starts with time interval2 then time interval2 starts with time interval1 ')
(forall ((t1 "time interval") (t2 "time interval"))
(if ("time interval1 starts with time interval2" t1 t2)
("time interval2 starts with time interval1" t2 t1) ))
(cl:comment 'time interval1 finishes with time interval2
Definition: time interval1 finishes time interval2 or time interval2 finishes time interval1 or time interval1 equals time interval2 '
)
(forall (t1 t2)
(iff ("time interval1 finishes with time interval2" t1 t2)
(or
("time interval1 finishes time interval2" t1 t2)
("time interval1 finishes time interval2" t2 t1)
("time interval1 equals time interval2" t1 t2)) ))
(cl:comment 'Necessity: If time interval1 finishes with time interval2 then time interval2 finishes with time interval1 ')
(forall ((t1 "time interval") (t2 "time interval"))
(if ("time interval1 finishes with time interval2" t1 t2)
("time interval2 finishes with time interval1" t2 t1) ))
(cl:comment 'time interval1 finishes after time interval2
Definition: some time interval3 is part of time interval1 and is after time interval2 ')
(forall (t1 t2)
(iff ("time interval1 finishes after time interval2" t1 t2)
(exists (t3)
(and
("time interval1 is before time interval2" t2 t3)
("time interval1 is part of time interval2" t3 t1) ))))
(cl:comment 'some time interval3 finishes time interval1 and is part of time interval2')
(forall (t1 t2)
(iff ("time interval1 ends during time interval2" t1 t2)
(exists (t3)
(and
("time interval1 finishes time interval2" t3 t1)
("time interval1 is part of time interval2" t3 t2) ))))
(cl:comment 'time interval1 follows time interval2 and time interval1 precedes time interval3 ')
(forall (t1 t2 t3)
(iff ("time interval1 is between time interval2 and time interval3" t1 t2 t3)
(and
("time interval" t1) ("time interval" t2)
("time interval" t3)
("time interval1 precedes time interval2" t2 t1)
("time interval1 precedes time interval2" t1 t3))))
(cl:comment 'time interval3 includes time interval1 and time interval3 includes time interval2 and time interval3 is part of each time interval that includes time interval1 and time interval2')
(forall (t1 t2 t3)
(iff ("time interval1 plus time interval2 is time interval3" t1 t2 t3)
(and
("thing1 is part of thing2" t1 t3)
("thing1 is part of thing2" t2 t3)
(forall (t4)
(if (and
("thing1 is part of thing2" t1 t4)
("thing1 is part of thing2" t2 t4))
("thing1 is part of thing2" t3 t4)))
)))
(cl:comment 'Necessity:if a time interval1 is before a time interval2 or time interval1 properly overlaps time interval2, then time interval1 plus time interval2 is started by time interval1 and is finished by time interval2')
(forall (t1 t2 t3)
(if
(or
("time interval1 is before time interval2" t1 t2)
("time interval1 properly overlaps time interval2" t1 t2))
(iff
("time interval1 plus time interval2 is time interval3" t1 t2 t3)
(and
("time interval1 starts time interval2" t1 t3)
("time interval1 finishes time interval2" t2 t3))
)))
(cl:comment 'Necessity: if a time interval1 is after a time interval2 or time interval1 is properly overlapped by time interval2, then time interval1 plus time interval2 is started by time interval2 and is finished by time interval1.')
(forall (t1 t2 t3)
(if
(or
("time interval1 is before time interval2" t2 t1)
("time interval1 properly overlaps time interval2" t2 t1))
(iff
("time interval1 plus time interval2 is time interval3" t1 t2 t3)
(and
("time interval1 starts time interval2" t2 t3)
("time interval1 finishes time interval2" t1 t3))
)))
(cl:comment 'Necessity: if a time interval1 is part of a time interval2, then time interval1 plus time interval2 is time interval2.')
(forall (t1 t2 t3)
(if
("time interval1 is part of time interval2" t1 t2)
(iff
("time interval1 plus time interval2 is time interval3" t1 t2 t3)
(= t3 t2)
)))
(cl:comment 'Necessity: if a time interval2 is part of a time interval1, then time interval1 plus time interval2 is time interval1.')
(forall (t1 t2 t3)
(if
("time interval1 is part of time interval2" t2 t1)
(iff
("time interval1 plus time interval2 is time interval3" t1 t2 t3)
(= t3 t1)
)))
(cl:comment 'For each time interval1 and each time interval2, there is a time interval3 that is time interval1 plus time interval2.')
(forall ((t1 "time interval") (t2 "time interval"))
(exists ((t3 "time interval"))
("time interval1 plus time interval2 is time interval3" t1 t2 t3) ))
(cl:comment 'A time interval1 plus a time interval2 is exactly one time interval3.')
(forall (t1 t2 t3)
(if ("time interval1 plus time interval2 is time interval3"
t1 t2 t3)
(forall (t4)
(if
("time interval1 plus time interval2 is time interval3"
t1 t2 t4)
(= t4 t3) )) ))
(cl:comment 'time interval1 starts time interval2 and time interval3 finishes the time interval2 and time interval1 meets time interval3')
(forall (t1 t2 t3)
(iff ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
(and
("time interval1 starts time interval2" t1 t2)
("time interval1 finishes time interval2" t3 t2)
("time interval1 meets time interval2" t1 t3)) ))
(cl:comment 'if a time interval1 starts a time interval2 then some time interval3 finishes time interval2 complementing time interval1')
(forall (t1 t2)
(if ("time interval1 starts time interval2" t1 t2)
(exists (t3)
("time interval1 starts time interval2 complementing time interval3" t1 t2 t3) )))
(cl:comment 'If a time interval1 starts a time interval2 complementing a time interval3, then each time interval4 that is part of the time interval2 and that does not overlap the time interval1 is part of the time interval3.')
(forall (t1 t2 t3)
(if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
(forall (t4)
(if
(and
("time interval1 is part of time interval2" t4 t2)
(not ("time interval1 overlaps time interval2" t4 t1)))
("time interval1 is part of time interval2" t4 t3)))))
(cl:comment 'If a time interval1 starts a time interval2 then the time interval1 starts the time interval2 complementing exactly one time interval3.')
(forall (t1 t2 t3)
(if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
(forall (t4)
(if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t4)
(= t4 t3))) ))
(cl:comment 'time interval1 finishes time interval2 and time interval3 starts time interval2 and time interval1 is met by time interval3')
(forall (t1 t2 t3)
(iff ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
(and
("time interval1 finishes time interval2" t1 t2)
("time interval1 starts time interval2" t3 t2)
("time interval1 meets time interval2" t3 t1)) ))
(cl:comment 'if the time interval1 finishes the time interval2 then some time interval3 starts time interval2 complementing time interval1')
(forall (t1 t2)
(if ("time interval1 finishes time interval2" t1 t2)
(exists (t3)
("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3) )))
(cl:comment 'If a time interval1 finishes a time interval2 complementing a time interval3, then each time interval4 that is part of the time interval2 and that does not overlap the time interval1 is part of the time interval3.')
(forall (t1 t2 t3)
(if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
(forall (t4)
(if
(and
("time interval1 is part of time interval2" t4 t2)
(not ("time interval1 overlaps time interval2" t4 t1)))
("time interval1 is part of time interval2" t4 t3)))))
(cl:comment 'If a time interval1 finishes a time interval2 then the time interval1 finishes the time interval2 complementing exactly one time interval3.')
(forall (t1 t2 t3)
(if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
(forall (t4)
(if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t4)
(= t4 t3))) ))
(cl:comment 'For each time interval1 and each time interval2 that is properly during time interval1, there is a time interval4 that finishes time interval1 and is met by time interval2.')
(forall ((ti1 "time interval")
(ti2 "time interval"))
(if ("time interval1 is properly during
time interval2" t2 t1)
(exists (ti3 "time interval")
(and
("time interval1 starts time interval2" ti3 ti1)
("time interval1 meets time interval2"
ti3 ti2) )) ))
(cl:comment 'For each time interval1 and each time interval2 that is properly during time interval1, there is a time interval4 that finishes time interval1 and is met by time interval2.')
(forall ((ti1 "time interval")
(ti2 "time interval"))
(if ("time interval1 is properly during time interval2" t2 t1)
(exists (ti4 "time interval")
(and
("time interval1 finishes time interval2" ti4 ti1)
("time interval1 meets time interval2"
ti2 ti4) )) ))
(cl:comment 'Definition: time interval1 is part of time interval2 and time interval1 is part of time interval3 and time interval1 includes each time interval that is part of time interval2 and time interval3')
(forall (t1 t2 t3)
(iff
("time interval1 intersects time interval2 with time interval3"
t1 t2 t3)
(and
("thing1 is part of thing2" t1 t2)
("thing1 is part of thing2" t1 t3)
(forall (t4)
(if (and
("thing1 is part of thing2" t4 t2)
("thing1 is part of thing2" t4 t3))
("thing1 is part of thing2" t4 t1) ))
)))
(cl:comment 'Definition: if time interval2 is part of time interval3, then time interval1 equals time interval3, and
if time interval3 is part of time interval2, then time interval1 equals time interval2, and
if time interval2 properly overlaps time interval3, then time interval1 finishes time interval2 and time interval1 starts time interval3, and
if time interval3 properly overlaps time interval2, then time interval1 finishes time interval3 and time interval1 starts time interval2')
(forall (t1 t2 t3)
(iff
("time interval1 intersects time interval2 with time interval3"
t1 t2 t3)
(and
(if ("thing1 is part of thing2" t2 t3) (=t1 t2))
(if ("thing1 is part of thing2" t3 t2) (=t1 t3))
(if ("time interval1 properly overlaps time interval2" t2 t3)
(and
("time interval1 finishes time interval2" t1 t2)
("time interval1 starts time interval2" t1 t3)) )
(if ("time interval1 properly overlaps time interval2" t3 t2)
(and
("time interval1 finishes time interval2" t1 t3)
("time interval1 starts time interval2" t1 t2)) )
)))
(cl:comment 'if a time interval1 overlaps a time interval2, then some time interval3 intersects time interval1 with time interval2')
(forall (t1 t2)
(if
("time interval1 overlaps time interval2" t1 t2)
(exists (t3)
("time interval1 intersects time interval2 with time interval3"
t3 t1 t2) )))
(cl:comment 'If a time interval1 intersects a time interval2 with a time interval3 and a time interval4 is part of the time interval1 and the time interval4 is part of the time interval2, then the time interval4 is part of the time interval3.')
(forall (t1 t2 t3 t4)
(if
(and
("time interval1 intersects time interval2 with time interval3"
t1 t2 t3)
("time interval1 is part of time interval2" t4 t2)
("time interval1 is part of time interval2" t4 t1))
("time interval1 is part of time interval2" t4 t3) ))
(cl:comment 'If a time interval1 overlaps a time inteval2, then the time interval1 intersects a time interval2 with exactly one time interval3.')
(forall (t1 t2 t3)
(if
("time interval1 intersects time interval2 with time interval3"
t3 t1 t2)
(forall (t4)
(if
("time interval1 intersects time interval2 with time interval3"
t4 t1 t2)
(= t4 t3))) ))
(cl:comment 'If a time interval1 is properly before a time interval2 then the time interval1 meets a time interval3 and the time interval3 meets the time interval2 and the time interval1 plus the time interval2 is a time interval4 and the time interval1 starts the time interval4 complementing a time interval5 and the time interval2 finishes the time interval4 complementing a time interval6 and the time interval5 intersects the time interval6 with the time interval3.')
(forall (t1 t2)
(if ("time interval1 is properly before time interval2" t1 t2)
(exists (t3 t4 t5 t6)
(and
("time interval1 meets time interval2" t1 t3)
("time interval1 meets time interval2" t3 t2)
("time interval1 plus time interval2 is time interval3"
t1 t2 t4)
("time interval1 finishes time interval2 complementing time interval3" t5 t4 t1)
("time interval1 starts time interval2 complementing time interval3" t6 t4 t2)
("time interval1 intersects time interval2 with time interval3" t3 t6 t5))) ))
(cl:commment 'time interval1 starts before time interval2, and
time interval1 starts time interval3, and
time interval2 finishes time interval3')
(forall (t1 t2 t3)
(iff
("time interval1 through time interval2 specifies time interval3" t1 t2 t3)
(and
("time interval1 starts before time interval2" t1 t2)
("time interval1 starts time interval2" t1 t3)
("time interval1 finishes time interval2" t2 t3)
)))
(cl:comment 'time interval1 through time interval2')
(forall (t1 t2 t3)
(iff (= t3 ("time interval1 through time interval2" t1 t2))
("time interval1 through time interval2 specifies time interval3" t1 t2 t3) ))
(cl:comment 'Necessity: For each time interval1 that starts before a given time interval2, exactly one time interval3 is time interval1 through time interval2.')
(forall (t1 t2)
(if ("time interval1 starts before time interval2" t1 t2)
(exists (t3)
("time interval1 is time interval2 through time interval3"
t3 t1 t2) )))
(forall (t1 t2 t3 t4)
(if (and
("time interval1 is time interval2 through time interval3"
t3 t1 t2)
("time interval1 is time interval2 through time interval3"
t4 t1 t2) )
(= t3 t4) ))
(cl:comment 'Definition: time interval1 is before time interval2, and
time interval3 is time interval1 if time interval1 meets time interval2, and
time interval3 is the time interval that meets time interval2 and is started by time interval1 if time interval1 is properly before time interval2')
(forall (t1 t2 t3)
(iff
("time interval1 to time interval2 specifies time interval3" t1 t2 t3)
(and
("time interval1 is before time interval2" t1 t2)
(if ("time interval1 meets time interval2" t1 t2)
(= t1 t3))
(if
("time interval1 is properly before time interval2" t1 t2)
(and
("time interval1 starts time interval2" t1 t3)
("time interval1 meets time interval2" t3 t2)
))
)))
(cl:comment 'time interval1 to time interval2')
(forall (t1 t2 t3)
(iff (= t3 ("time interval1 to time interval2" t1 t2))
("time interval1 to time interval2 specifies time interval3"
t1 t2 t3) ))
(cl:comment 'Necessity: For each time interval1 that is before a given time interval2, exactly one time interval3 is time interval1 to time interval2.')
(forall (t1 t2)
(if ("time interval1 is before time interval2" t1 t2)
(exists (t3)
("time interval1 is time interval2 to time interval3"
t3 t1 t2) )))
(forall (t1 t2 t3 t4)
(if (and
("time interval1 is time interval2 to time interval3"
t3 t1 t2)
("time interval1 is time interval2 to time interval3"
t4 t1 t2) )
(= t3 t4) ))
(cl:comment 'the time interval that includes each time interval')
(forall (t) (iff (= t eternity)
(and
("time interval" t)
(forall (ti2) (iff ("time interval" ti2)
("is part of" ti2 t) ))
)))
(cl:comment 'the time interval that is before each time interval that is not primordiality or eternity')
(forall (t)
(iff (= t primordiality)
(and
("time interval" t)
(forall (ti2) (or
(= ti2 primordiality)
(= ti2 eternity)
("time interval1 is before time interval2" t ti2) )))))
(cl:comment 'the time interval that is after each time interval that is not perpetuity or eternity')
(forall (t)
(iff (= t perpetuity)
(and
("time interval" t)
(forall (ti2) (or
(= ti2 perpetuity)
(= ti2 eternity)
("time interval1 is before time interval2" ti2 t) )))))
(cl:comment 'Each duration <= the duration.')
(forall ((d1 duration))
(<= d1 d1))
(cl:comment 'Each duration1 <= each duration2 or duration2 <= duration1.')
(forall ((d1 duration) (d2 duration))
(or
(<= d1 d2)
(<= d2 d1)))
(cl:comment 'If some duration1 <= some duration2 and the duration2 <= the duration1, then the duration1 equals the duration2.')
(forall ((d1 duration) (d2 duration))
(if (and
("duration1 <= duration2" d1 d2)
("duration1 <= duration2" d2 d1))
(= d1 d2)))
(cl:comment 'If some duration1 <= some duration2 and the duration2 <= the duration3 then the duration1 <= the duration3.')
(forall ((d1 duration) (d2 duration) (d3 duration))
(if (and
("duration1 <= duration2" d1 d2)
("duration1 <= duration2" d2 d3))
("duration1 <= duration2" d1 d3)))
(cl:comment 'If some duration1 = some duration2 and the duration2 = some duration3 then the duration1 = the duration3.')
(forall (d1 d2 d3)
(if (and
("duration = duration" d1 d2)
("duration = duration" d2 d3))
("duration = duration" d1 d3)))
(cl:comment 'duration1 <= duration2 and duration1 does not equal duration2 ')
(forall ((d1 duration) (d2 duration))
(iff ("duration1 < duration2" d1 d2)
(and
("duration1 <= duration2" d1 d2)
(not (= d2 d1)))))
(cl:comment 'duration3 equals duration1 plus duration2')
(forall ((d1 duration) (d2 duration) d3)
(iff
(= d3 (+ d1 d2))
(and
(duration d3)
("duration3 = duration1 + duration2"
d3 d1 d2) )))
(cl:comment 'For each duration1 and each duration2 some duration3 equals duration1 plus duration2.')
(forall ((d1 duration) (d2 duration))
(exists (d3 duration) (= d3 (+ d1 d2))))
(cl:comment 'If a duration4 equals a duration1 plus a duration2, and a duration5 equals duration4 plus duration3, and a duration6 equals duration2 plus duration3, then duration5 equals duration1 plus duration6.')
(forall ((d1 duration) (d2 duration) (d3 duration))
(= (+ (+ d1 d2) d3) (+ d1 (+ d2 d3))) )
(cl:comment 'Each duration1 plus duration2 equals duration2 plus duration1.')
(forall ((d1 duration))
(exists ((d2 duration))
(= D0 (+ d1 d2))))
(cl:comment 'Each duration plus D0 = the duration.')
(and
(duration D0)
(forall (d duration) (= (+ d D0) d) ))
(cl:comment 'duration1 equals duration3 plus duration2')
(forall ((d1 duration) (d2 duration) d3)
(iff
(= d3 (- d1 d2))
(and
(duration d3)
("duration3 = duration1 - duration2"
d3 d1 d2) )))
(cl:comment 'D0 equals each duration1 plus some duration2.')
(forall ((d1 duration))
(exists ((d2 duration))
(= D0 (+ d1 d2))))
(cl:comment 'duration2 is the result of duration1 plus duration1, repeated number times')
(forall ((d1 duration) (n number) d2)
(iff
(= d2 (times n d1))
(and
(duration d2)
("duration2 = number times duration1" d2 n d1) )))
(cl:comment 'For each number and each duration1, there is a duration2 that is number times duration1.')
(forall ((n1 number) (d1 duration))
(exists ((d2 duration))
(= d2 (times n1 d1))))
(cl:comment 'If a duration3 equals a number1 times (a duration1 plus a duration2) then duration3 equals (number1 times duration1) plus (number1 times duration2).')
(forall ((d1 duration) (d2 duration)
(d3 duration) (n1 number))
(if (= d3 (times n1 (+ d1 d2)))
(= d3 (+ (* n1 d1) (times n1 d2)))))
(cl:comment 'If a (number1 plus a number2) times a duration1 equals a duration2, then duration2 equals (number1 times duration1) plus (number2 times duration1).')
(forall ((d1 duration) (n1 number) (n2 number))
(= (times (+ n1 n2) d1) (+ (times n1 d1) (times n2 d1))))
(cl:comment 'D0 equals 0 times each duration1.')
(forall ((d1 duration))
(times 0 d1 D0))
(cl:comment 'D0 equals a number1 times a duration1 if and only if number1 equals 0 or duration1 equals D0.')
(forall ((n1 number) (d1 duration))
(iff (= D0 (times n1 d1))
(or
(= n1 0)
(= d1 D0)) ))
(cl:comment 'If a duration1 does not equal D0, then a duration2 equals a number1 times duration1.')
(forall ((d1 duration))
(if (not (= d1 D0))
(exists ((d2 duration) (n1 number))
(times d1 n1 d2))))
(cl:comment 'the particular duration is the duration that is the amount of time in the time interval')
(forall (d ti) (iff
(= d ("duration of time interval" ti))
(and
("time interval" ti) (duration d)
("time interval has duration" ti d) )))
(cl:comment 'the particular duration is the duration that is the amount of time in the time interval')
(forall (t d)
(if ("time interval has duration" t d)
(and ("time interval" t) (duration d)) ))
(forall (t d)
(iff (= ("duration of" t) d)
("time interval has duration" t d)))
(cl:comment 'Each time interval has exactly one duration.')
(forall ((t "time interval") (d1 duration) (d2 duration))
(if (and ("time interval has duration" t d1)
("time interval has duration" t d2))
(= d1 d2)))
(cl:comment 'The duration of each time interval is greater than D0.')
(forall ((t "time interval"))
(> ("duration of" t) D0))
(cl:comment 'The duration of no time interval equals D0.')
(forall ((t "time interval"))
(not (= ("duration of" t) D0)))
(cl:comment 'For each time interval1 there is no time interval2 such that the duration of time interval1 plus the duration of time interval2 equals D0.')
(not (exists ((t1 t2))
("duration3 = duration1 plus duration2"
D0 ("duration of time interval" t1)
("duration of time interval" t2)) ))
(cl:comment 'For each time interval1 and each time interval2 that is a part of time interval1, the duration of time interval2 is less than or equal to the duration of time interval1.')
(forall (t1 t2)
(if ("time interval1 is part of time interval2" t1 t2)
("duration1 <= duration2"
("duration of" t1) ("duration of" t2)) ))
(cl:comment 'For each time interval1 and each time interval2 that meets a time interval1, the duration of time interval1 plus time interval2 is equal to the duration of time interval1 plus the duration of time interval2.')
(forall (t1 t2 t3)
(if (and
("time interval1 meets time interval2" t1 t2)
("time interval3 equals time interval1 plus time interval2" t3 t1 t2))
(= (+ ("duration of" t1) ("duration of" t2))
("duration of" t3)) ))
(cl:comment 'For each time interval2 and each time interval3 that finishes time interval2, the duration of the time interval1 that starts time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.')
(forall (t1 t2 t3)
(if ("time interval1 starts time interval2 complementing time interval3" t1 t2 t3)
(= ("duration of" t1)
(- ("duration of" t2) ("duration of" t3)) ) ))
(cl:comment 'For each time interval2 and each time interval3 that starts time interval2, the duration of the time interval1 that finishes time interval2 complementing time interval3 is equal to the duration of time interval2 minus the duration of time interval3.')
(forall (t1 t2 t3)
(if ("time interval1 finishes time interval2 complementing time interval3" t1 t2 t3)
(= ("duration of" t1)
(- ("duration of" t2) ("duration of" t3)) ) ))
(cl:comment 'time interval2 is duration before time interval1
Definition: time interval1 meets some time interval3 that has the duration and meets time interval2 ')
(forall (t1 t2 d)
(iff ("time interval2 is duration before time interval1" t1 d t2)
(and
("time interval" t1)
("time interval" t2)
(duration d)
("time interval1 is before time interval2" t2 t1)
(exists ("time interval" t3)
(and
("time interval1 meets time interval2" t2 t3)
("time interval1 meets time interval2" t3 t1)
("duration1 equals duration2" d ("duration of" t3))
)))))
(cl:comment 'time interval1 starts duration before time interval2
Definition: time interval1 starts with the time interval3 that has the duration and meets time interval2 '
)
(forall (t1 t2 d)
(iff ("time interval1 starts duration before time interval2" t1 d t2)
(and
("time interval" t1) ("time interval" t2) (duration d)
(exists (t3 "time interval")
(and
("time interval1 meets time interval2" t3 t2)
("time interval1 starts with time interval2" t1 t3)
("time interval has duration" t3 d)
)))))
(cl:comment 'time interval1 finishes duration after time interval2
Definition: time interval1 finishes with the time interval3 that has the duration and is met by time interval2 '
)
(forall (t1 t2 d)
(iff ("time interval1 finishes duration after time interval2" t1 d t2)
(and
("time interval" t1) ("time interval" t2) (duration d)
(exists (t3 "time interval")
(and
("time interval1 meets time interval2" t3 t2)
("time interval1 finishes with time interval2" t1 t3)
("time interval has duration" t3 d)
)))))
(cl:comment 'time interval1 is the duration preceding time interval2
Definition: time interval1 is the time interval that has the duration and meets time interval2 ')
)
(forall (t1 t2 d)
(iff ("time interval1 is the duration preceding time interval2" t1 d t2)
(and
("time interval" t1)
("time interval" t2)
(duration d)
("time interval1 meets time interval2" t1 t2)
("time interval has duration" t1 d) )))
(cl:comment 'For each time interval2 and for each duration, exactly one time interval1 is the duration preceding time interval2.')
(forall (t1 d) (exists (t2)
(and
("time interval1 is the duration preceding time interval2" t2 d t1)
(forall (t3)
(if
("time interval1 is the duration preceding time interval2" t3 d t1)
(= t3 t2) ))
)))
(cl:comment 'time interval1 is the duration following time interval2
Definition: time interval1 is the time interval that has the duration and is met by time interval2 '
)
(forall (t1 t2 d)
(iff ("time interval1 is the duration following time interval2" t1 d t2)
(and
("time interval" t1)
("time interval" t2)
(duration d)
("time interval1 meets time interval2" t2 t1)
("time interval has duration" t1 d) )))
(cl:comment 'For each time interval2 and for each duration, exactly one time interval1 is the duration following time interval2.')
(forall (t1 d) (exists (t2)
(and
("time interval1 is the duration following time interval2" t2 d t1)
(forall (t3)
(if
("time interval1 is the duration following time interval2" t3 d t1)
(= t3 t2) ))
)))
(cl:comment '*** Situations ***')
(cl:comment 'the occurrence is a realization of the situation kind')
(forall (s occ)
(if ("situation kind has occurrence" s occ)
(and ("situation kind" s) (occurrence occ)) ))
(cl:comment 'the occurrence happens continuously, without interruption, in each time interval2 that is part of the time interval')
(forall (occ ti)
(if ("occurrence occurs throughout time interval" occ ti)
(and (occurrence occ) ("time interval" ti)) ))
(cl:comment 'the occurrence occurs throughout some time interval2 that is part of the time interval')
(forall (occ t1)
(iff ("occurrence occurs within time interval" occ t1)
(and
(occurrence occ) ("time interval" t1)
(exists (t2)
(and
("time interval1 is part of time interval2" t2 t1)
("occurrence occurs throughout time interval"
occ t2))) )))
(cl:comment 'the occurrence occurs throughout the occurrence interval and the occurrence does not occur within some time interval2 that meets the occurrence interval and the occurrence does not occur within some time interval3 that is met by the occurrence interval')
(forall (occ t1)
(iff ("occurrence occurs for occurrence interval" occ t1)
(and
("occurrence occurs throughout time interval" occ t1)
(exists (t2 t3)
(and
("time interval1 meets time interval2" t2 t1)
(not ("occurrence occurs within time interval" occ t2))
("time interval1 meets time interval2" t1 t3)
(not ("occurrence occurs within time interval" occ t3))
)) )))
(cl:comment 'Each occurrence occurs for exactly one occurrence interval.')
(forall (occ) (exists (t)
(and
("occurrence occurs for occurrence interval" occ t)
(forall (t2)
(if (occurrence occurs for occurrence interval" occ t2)
(= t2 t)))
)))
(cl:comment 'the occurrence occurs for some occurrence interval and the duration is the duration of the occurrence interval')
(forall (occ d)
(iff ("occurrence lasts for duration" occ d)
(and
(occurrence occ) (duration d)
(exists (t)
(and
("occurrence occurs for time interval" occ t)
("time interval has duration" t d))))))
(cl:comment 'the occurrence interval of the occurrence is before the time interval')
(forall (occ ti) (iff
("occurrence occurs before time interval" occ ti)
(and
(occurrence occ)
("time interval" ti)
("time interval is before time interval"
("occurrence interval" occ) ti) )))
(cl:comment 'the occurrence interval of the occurrence is after the time interval')
(forall (occ ti) (iff
("occurrence occurs after time interval" occ ti)
(and
(occurrence occ)
("time interval" ti)
("time interval is before time interval"
ti ("occurrence interval" occ)) )))
(cl:comment 'the occurrence interval of the occurrence starts during the time interval')
(forall (occ ti)
(iff ("occurrence starts during time interval" occ ti)
(exists (ti2)
(and
("occurrence occurs for occurrence interval" occ ti2)
("time interval1 starts during time interval2" ti2 ti) ))))
(cl:comment 'the occurrence interval of the occurrence ends during the time interval')
(forall (occ ti)
(iff ("occurrence ends during time interval" occ ti)
(exists (ti2)
(and
("occurrence occurs for occurrence interval" occ ti2)
("time interval1 ends during time interval2" ti2 ti) ))))
(cl:comment 'the occurrence interval of occurrence1 precedes the occurrence interval of occurrence2')
(forall (o1 o2)
(iff ("occurrence1 precedes occurrence2" o1 o2)
(and
(occurrence o1) (occurrence o2)
(forall (t1 t2)
(if
(and
("occurrence occurs for time interval" o1 t1)
("occurrence occurs for time interval" o2 t2))
("time interval1 precedes time interval2" t1 t2)))
)))
(cl:comment 'If some occurrence1 precedes some occurrence2, and if the occurrence2 precedes some occurrence3, then occurrence1 precedes occurrence3.')
(forall (o1 o2 o3)
(if (and
("occurrence1 precedes occurrence2" o1 o2)
("occurrence1 precedes occurrence2" o2 o3))
("occurrence1 precedes occurrence2" o1 o3)))
(cl:comment 'the occurrence interval of occurrence1 starts before the occurrence interval of occurrence2')
(forall (o1 o2)
(iff ("occurrence1 starts before occurrence2" o1 o2)
(and
(occurrence o1) (occurrence o2)
(forall (t1 t2)
(if
(and
("occurrence occurs for time interval" o1 t1)
("occurrence occurs for time interval" o2 t2))
("time interval1 starts before time interval2" t1 t2)))
)))
(cl:comment 'the occurrence interval of occurrence1 ends before the occurrence interval of occurrence2 ')
(forall (o1 o2)
(iff ("occurrence1 ends before occurrence2" o1 o2)
(and
(occurrence o1) (occurrence o2)
(forall (t1 t2)
(if
(and
("occurrence occurs for time interval" o1 t1)
("occurrence occurs for time interval" o2 t2))
("time interval1 ends before time interval2" t1 t2)))
)))
(cl:comment 'the occurrence interval of occurrence1 overlaps the occurrence interval of occurrence2')
(forall (o1 o2)
(if ("o1 overlaps o2")
(and
(occurrence o1)
(occurrence o2)
(forall ((t1 "time interval")
(t2 "time interval"))
(if (and
("occurrence occurs for time interval" o1 t1)
("occurrence occurs for time interval" o2 t2))
("time interval1 overlaps time interval2" t1 t2))))))
(cl:comment 'occurrence1 follows occurrence2 and occurrence1 precedes occurrence3')
(forall (o1 o2 o3)
(iff ("occurrence1 is between occurrence2 and occurrence3"
o1 o2 o3)
(and
("occurrence precedes occurrence" o2 o1)
("occurrence precedes occurrence" o1 o3)) ))
(cl:comment 'each occurrence of situation kind1 precedes each occurrence of situation kind2 ')
(forall (s1 s2)
(iff ("situation kind1 precedes situation kind2" s1 s2)
(forall (o1 o2)
(if
(and
("situation kind has occurrence" s1 o1)
("situation kind has occurrence" s2 o2))
("occurrence1 precedes occurrence2" o1 o2)) )))
(cl:comment 'the first occurrence exemplifies the situation kind and the first occurrence occurs after the time interval and no occurrence that exemplifies the situation kind and that occurs after the time interval starts before the first occurrence')
(forall (sk fo ti) (iff
('situation kind has first occurrence after time interval' sk fo ti)
(and
('occurrence exemplifies situation kind' fo sk)
('occurrence occurs after time interval' fo ti)
(not (exists (occ) (and
('occurrence exemplifies situation kind' occ sk)
('occurrence occurs after time interval' occ ti)
('occurrence1 starts before occurrence2' occ fo)
))) )))
(cl:comment 'the first occurrence exemplifies the situation kind and no occurrence that exemplifies the situation kind starts before the first occurrence')
(forall (sk fo) (iff
('situation kind has first occurrence' sk fo)
(and
('occurrence exemplifies situation kind' fo sk)
(not (exists (occ) (and
('occurrence exemplifies situation kind' occ sk)
('occurrence1 starts before occurrence2' occ fo)
))) )))
(cl:comment 'each occurrence of situation kind1 starts before each occurrence of situation kind')
(forall (s1 s2)
(iff ("situation kind1 starts before situation kind2" s1 s2)
(and
("situation kind" s1) ("situation kind" s2)
(forall (o1 o2)
(if
(and
("situation kind has occurrence" s1 o1)
("situation kind has occurrence" s2 o2))
("occurrence1 starts before occurrence2" o1 o2)))
)))
(cl:comment 'the last occurrence exemplifies the situation kind and no occurrence that exemplifies the situation kind ends after the last occurrence')
(forall (sk fo) (iff
('situation kind has last occurrence' sk lo)
(and
('occurrence exemplifies situation kind' lo sk)
(not (exists (occ) (and
('occurrence exemplifies situation kind' occ sk)
('occurrence1 ends before occurrence2' lo occ)
))) )))
(cl:comment 'the last occurrence exemplifies the situation kind and the last occurrence occurs before the time interval and no occurrence that exemplifies the situation kind and that occurs before the time interval ends after the last occurrence')
(forall (sk lo ti) (iff
('situation kind has last occurrence before time interval' sk lo ti)
(and
('occurrence exemplifies situation kind' lo sk)
('occurrence occurs before time interval' lo ti)
(not (exists (occ) (and
('occurrence exemplifies situation kind' occ sk)
('occurrence occurs before time interval' occ ti)
('occurrence1 ends before occurrence2' lo occ)
))) )))
(cl:comment 'each occurrence of situation kind1 precedes each occurrence of situation kind2 ')
(forall (s1 s2)
(iff ("situation kind1 precedes situation kind2" s1 s2)
(and
("situation kind" s1) ("situation kind" s2)
(forall (o1 o2)
(if
(and
("situation kind has occurrence" s1 o1)
("situation kind has occurrence" s2 o2))
("occurrence1 precedes occurrence2" o1 o2)))
)))
(cl:comment 'each occurrence of situation kind1 starts before each occurrence of situation kind')
(forall (s1 s2)
(iff ("situation kind1 starts before situation kind2" s1 s2)
(and
("situation kind" s1) ("situation kind" s2)
(forall (o1 o2)
(if
(and
("situation kind has occurrence" s1 o1)
("situation kind has occurrence" s2 o2))
("occurrence1 starts before occurrence2" o1 o2)))
)))
(cl:comment 'each occurrence of situation kind1 ends before each occurrence of situation kind2')
(forall (s1 s2)
(iff ("situation kind1 ends before situation kind2" s1 s2)
(and
("situation kind" s1) ("situation kind" s2)
(forall (o1 o2)
(if
(and
("situation kind has occurrence" s1 o1)
("situation kind has occurrence" s2 o2))
("occurrence1 ends before occurrence2" o1 o2)))
)))
(cl:comment 'each occurrence of situation kind1 overlaps some occurrence of situation kind2')
(forall (s1 s2)
(iff ("situation kind1 overlaps
situation kind2" s1 s2)
(and
("situation kind" s1)
("situation kind" s2)
(forall (o1 o2)
(and
(occurrence o1)
(occurrence o2)
(if (and
("situation kind has occurrence"
s1 o1)
("situation kind has occurrence"
s2 o2))
("occurrence1 overlaps occurrence2"
o1 o2)))))))
(cl:comment '---------------End DTV Vocabulary----------------------------')
)
(cl:text "Schedules"
(cl:import "Date-Time Vocabulary")
(cl:comment 'the schedule entry is in the schedule entry set of the schedule.')
(forall (s se)
(iff ("schedule has schedule entry" s se)
(exists (ses)
(and
("schedule entry set of schedule" ses s)
("thing is in set" se ses) ))))
(cl:comment 'Each schedule entry has exactly one situation kind.')
(forall (se) (exists (sk1)
(and ("schedule entry has situation kind" se sk1)
(forall (sk2)
(if ("schedule entry has situation kind" se sk2)
(= sk1 sk2) )))))
(cl:comment 'Each schedule entry has exactly one time interval.')
(forall (se) (exists (t1)
(iff ("schedule entry has time interval" se t1)
(forall (sk2)
(if ("schedule entry has time interval" se t2)
(= t1 t2) )))))
(cl:comment 'Each schedule entry set includes at least one schedule entry.')
(forall (seset) (exists (se)
("schedule entry set includes schedule entry" seset se)))
(cl:comment 'Each schedule defines exactly one schedule entry set.')
(forall (se) (exists (ses)
(and
("schedule entry has schedule entry set" se ses)
(forall (ses2)
(if ("schedule entry has schedule entry set" se ses2)
(= ses1 ses2) )))))
(cl:comment 'the occurrence exemplifies the situation kind of a schedule entry of the schedule and the occurrence interval of the occurrence overlaps the time interval of the schedule entry
Note: The occurrence may be in the past or may be planned for the future.')
(forall (s o)
(iff ("schedule has occurrence" s o)
(exists (("schedule entry" se) ("situation kind" sk))
(and
("schedule has schedule entry" s se)
("schedule entry has situation kind" s sk)
("occurrence exemplifies situation kind" o sk)
("time interval1 overlaps time interval2"
("occurrence interval" o) ("time interval" se))
))))
(cl:comment 'the earliest time is the time interval of some schedule entry of the schedule and the earliest time does not start after the time interval of each schedule entry of the schedule')
(forall (s et)
(iff ("schedule has earliest time" s et)
(and
(exists (se1)
(and
("schedule has schedule entry" s se1)
("schedule entry has time interval" se1 et)))
(forall (se2 ti2)
(if (and
("schedule has schedule entry" s se2)
("schedule entry has time interval" se2 ti2) )
(not ("time interval1 starts after time interval2" et ti2)) )
))))
(cl:comment 'earliest time of schedule')
(forall ((s schedule) (et "time interval"))
(iff (= et ("earliest time of schedule" s)
("schedule has earliest time" s et) ))
(cl:comment 'the latest time is the time interval of some schedule entry of the schedule and the latest time ends after the time interval of each schedule entry of the schedule')
(forall (s lt)
(iff ("schedule has latest time" s lt)
(and
(exists (se1)
(and
("schedule has schedule entry" s se1)
("schedule entry has time interval" se1 lt)))
(forall (se2 ti2)
(if (and
("schedule has schedule entry" s se2)
("schedule entry has time interval" se2 ti2) )
(not ("time interval1 ends after time interval2" ti2 lt)) )
))))
(cl:comment 'latest time of schedule')
(forall ((s schedule) (lt "time interval"))
(iff (= lt ("latest time of schedule" s)
("schedule has latest time" s lt) ))
(cl:comment 'the time span equals the earliest time of the schedule through the latest time of the schedule')
(forall (s ts)
(iff ("schedule has time span" s ts)
(and
("time interval" ts)
("time interval1 plus time interval2 is time interval3"
("earliest time of schedule" s)
("latest time of schedule" s)
ts ) )))
(cl:comment 'time span of schedule')
(forall ((ts "time interval") (s schedule))
(iff (= ts ("time span of schedule" s))
("schedule has time span" s ts) ))
(cl:comment 'Each schedule has exactly one time span.')
(forall (s) (exists (t1)
(and
("schedule has time span" s t1)
(forall (t2)
(if ("schedule has time span" s t2)
(= t1 t2))
))))
(cl:comment 'No regular schedule is an ad hoc schedule.')
(forall ((rs "regular schedule"))
(not ("ad hoc schedule" rs))
)
(cl:comment 'A regular schedule is for exactly one situation kind.')
(forall (rs sk1)
(if ("regular schedule is for situation kind" rs sk1)
(forall (sk2)
(if ("regular schedule is for situation kind" rs sk2)
(= sk1 sk2))
)))
(cl:comment 'Each regular schedule has exactly one start time.')
(forall (rs st1)
(if ("regular schedule has start time" rs st1)
(forall (st2)
(if ("regular schedule has start time" rs st2)
(= st1 st2))
))
)
(cl:comment 'Each regular schedule has exactly one recurrence duration.')
(forall (rs rd1)
(if ("regular schedule has recurrence duration" rs rd1)
(forall (rd2)
(if ("regular schedule has recurrence duration" rs rd2)
(= rd1 rd2))
)))
(cl:comment 'Each regular schedule has at most one recurrence count.')
(forall (rs rc1)
(if ("regular schedule has recurrence count" rs rc1)
(forall (rc2)
(if ("regular schedule has recurrence count" rs rc2)
(= rc1 rc2)) )))
(cl:comment 'Each regular schedule has at most one initial stub.')
(forall (rs is1)
(if ("regular schedule has initial stub" rs is1)
(forall (is2)
(if ("regular schedule has initial stub" rs is2)
(= is1 is2)) )))
(cl:comment 'Each regular schedule has at most one final stub.')
(forall (rs fs1)
(if ("regular schedule has final stub" rs fs1)
(forall (fs2)
(if ("regular schedule has final stub" rs fs2)
(= fs1 fs2)) )))
(cl:comment 'The schedule entry set of a regular schedule is the regular entry set of the regular schedule plus each initial stub of the regular schedule plus each final stub of the regular schedule. ')
(forall
(rs ses res)
(if (and
("regular schedule" rs)
("schedule defines schedule entry set" rs ses)
("regular schedule has regular entry set" rs res)
(exists (init) ("regular schedule has initial stub" rs init))
(exists (fin) ("regular schedule has final stub" rs fin)) )
(= ses (setplus (setplus res init) fin))
))
(cl:comment 'The schedule entry set of a regular schedule is the regular entry set of the regular schedule plus each initial stub of the regular schedule plus each final stub of the regular schedule. ')
(forall
(rs ses res)
(if (and
("regular schedule" rs)
("schedule defines schedule entry set" rs ses)
("regular schedule has regular entry set" rs res)
(exists (init) ("regular schedule has initial stub" rs init))
(not (exists (fin) ("regular schedule has final stub" rs fin))) )
(= ses (setplus res init))
))
(cl:comment 'The schedule entry set of a regular schedule is the regular entry set of the regular schedule plus each initial stub of the regular schedule plus each final stub of the regular schedule. ')
(forall (rs ses res)
(if (and
("regular schedule" rs)
("schedule defines schedule entry set" rs ses)
("regular schedule has regular entry set" rs res)
(not (exists (init) ("regular schedule has initial stub" rs init)))
(exists (fin) ("regular schedule has final stub" rs fin)) )
(= ses (setplus res fin))
))
(cl:comment 'The schedule entry set of a regular schedule is the regular entry set of the regular schedule plus each initial stub of the regular schedule plus each final stub of the regular schedule. ')
(forall (rs ses res)
(if (and
("regular schedule" rs)
("schedule defines schedule entry set" rs ses)
("regular schedule has regular entry set" rs res)
(not (exists (init) ("regular schedule has initial stub" rs init)))
(not (exists (fin) ("regular schedule has final stub" rs fin))) )
(= ses res)
))
(cl:comment 'No ad hoc schedule is a regular schedule.')
(forall (ahs "ad hoc schedule")
(not ("regular schedule" ahs))
)
(cl:comment '---------------End Schedules Vocabulary ----------------------------')
)
(cl:text "Sequences"
(cl:comment 'Each sequence position is of exactly one sequence.')
(forall (seq sp)
(if ("sequence has sequence position" seq sp)
(and
(sequence seq)
("sequence position" sp)
(forall (seq2)
(if ("sequence has sequence position" seq2 sp)
(= seq2 seq))) )))
(cl:comment 'If the index1 of some sequence position1 of some sequence equals the index2 of some sequence position2 of the sequence then sequence position1 is sequence position2.')
(forall (seq sp1 sp2 x1 x2)
(if
(and
("sequence has sequence position" seq sp1)
("sequence has sequence position" seq sp2)
("sequence position has index" sp1 x1)
("sequence position has index" sp2 x2)
(= x1 x2) )
(= sp1 sp2) ))
(cl:comment 'Each sequence position has exactly one index.')
(forall ((sp "sequence position"))
(exists ((x1 "integer"))
(and
("sequence position has index" sp x1)
(forall (x2)
(if ("sequence position has index" sp x2)
(= x1 x2)) ) )))
(cl:comment 'the index of sequence position1 is less than the index of sequence position2 .')
(forall (sp1 sp2 x1 x2)
(if
(and
("sequence position has index" sp1 x1)
("sequence position has index" sp2 x2) )
(iff ("sequence position1 precedes sequence position2" sp1 sp2)
(exists ((seq sequence))
(and
("sequence has sequence position" seq sp1)
("sequence has sequence position" seq sp2)
(< x1 x2) )) )))
(cl:comment 'Each sequence position has at most one next sequence position. ')
(forall (sp nsp)
(iff ("next sequence position succeeds sequence position" nsp sp)
(and
("sequence position1 precedes sequence position2" sp nsp)
(not (exists (sp2)
(and
("sequence position1 precedes sequence position2" sp sp2)
("sequence position1 precedes sequence position2" sp2 nsp)) )) )))
(cl:comment 'the member is the member of a sequence position of the sequence')
(forall ((s sequence) (member thing))
(iff ("sequence has member" s member)
(exists ((sp "sequence position"))
(and ("sequence has sequence position" s sp)
("sequence position has member" sp m)))))
(cl:comment 'The sequence has a sequence position that has an index that equals the index, and the sequence position has a member that is the member.')
(forall (member index s)
(iff ("member has index in sequence" member index s)
(and
(sequence s) (integer index)
(exists (sp)
(and
("sequence has sequence position" s sp)
("sequence position has index" sp index)
("sequence position has member" sp member)) ))))
(cl:comment 'member with index in sequence')
(forall (member index s)
(iff (= member ("member with index in sequence" index s))
("member has index in sequence" member index s) ))
(cl:comment 'The concept corresponds to each member of the sequence.')
(forall (s c)
(iff ("sequence is of concept" s c)
(and
(sequence s) (concept c)
(forall (member)
(if ("member participates in sequence" member s)
("meaning corresponds to thing" c member)))
)))
(cl:comment 'Each sequence has at most one index origin member.')
(forall (seq) (forall (iom)
(if ("sequence has index origin member" seq iom)
(and
(forall (m)
(if ("sequence has index origin member" seq m)
(= m iom) )) ))))
(cl:comment 'Each sequence has at most one index origin value.')
(forall (seq) (exists (iov)
(if ("sequence has index origin value" seq iov)
(and
(integer iov)
(forall (iv2)
(if ("sequence has index origin value" seq iv2)
(= iov iv2)) )))))
(cl:comment 'The index of the index origin position equals the index origin value of the sequence.')
(forall (s p)
(iff ("sequence has index origin position" s p)
(exists (iov)
(and
("sequence has index origin value" s iov)
("sequence position has index" p iov) ))))
(cl:comment 'sequence that each sequence position of the sequence that is not the first position of the sequence is next after a sequence position2, and the index of the sequence position equals 1 plus the index of the sequence position2')
(forall (s) (iff ("consecutive sequence" s)
(and
(sequence s)
(forall (sp1)
(if
(and
("sequence has sequence position" s sp1)
(exists (sp2)
("next sequence position succeeds sequence position" sp2 sp1)) )
(forall (x1 x2)
(if
(and
("sequence position has index" sp1 x1)
("sequence position has index" sp2 x2))
(= x2 (+ x1 1)) ))
)) )))
(cl:comment 'sequence that each member of the sequence is the member of at most one sequence position of the sequence')
(forall (s) (iff ("unique sequence" s)
(and
(sequence s)
(forall (sp1 sp2 t1 t2)
(if
(and
("sequence has sequence position" s sp1)
("sequence has sequence position" s sp2)
("sequence position has member" sp1 t1)
("sequence position has member" sp2 t2)
(not (= sp1 sp2)) )
(not (= t1 t2)) )))))
(cl:comment 'Each thing has at most one index in each unique sequence.')
(forall (thing (x1 integer) (x2 integer) (us "unique sequence"))
(if (and
("member has index in sequence" thing x1 us)
("member has index in sequence" thing x2 us) )
(= x1 x2) ))
(cl:comment 'consecutive sequence that is a unique sequence')
(forall (s) (iff ("regular sequence" s)
(and
("consecutive sequence" s)
("unique sequence" s))))
(cl:comment 'member1 participates in the unique sequence and member2 participates in the unique sequence and each sequence position1 of member1 in the unique sequence precedes each sequence position2 of member2 in the unique sequence')
(forall ((s sequence) (m1 thing) (m2 thing))
(iff ("member1 precedes member2 in unique sequence" m1 m2 s)
(and
("member participates in sequence" m1 s)
("member participates in sequence" m2 s)
(forall ((sp1 "sequence position") (sp2 "sequence position"))
(if
(and
("sequence position of member" sp1 m1)
("sequence position of member" sp2 m2))
("sequence position1 precedes sequence position2" sp1 sp2) )))))
(cl:comment 'the first member is the member of the first position of the sequence')
(forall (s m)
(iff ("sequence has first member" s m)
(exists (first)
(and
("sequence has first position" s first)
("sequence position has member" first m)))))
(cl:comment 'the last member is the member of the last position of the sequence')
(forall (s m)
(iff ("sequence has last member" s m)
(exists (last)
(and
("sequence has last position" s last)
("sequence position has member" last m)))))
(cl:comment 'thing is the member of exactly one sequence position in the unique sequence and next member is the member of some sequence position of the unique sequence that succeeds the sequence position of the thing')
(forall (s nm m)
(iff
("next member is next after thing in unique sequence" nm m s)
(and
("unique sequence" s)
(exists (sp nsp)
(and
("sequence has sequence position" s sp)
("sequence position has member" sp m)
("next sequence position succeeds sequence position" nsp sp)
("sequence position has member" nsp nm) )))))
(cl:comment 'The last member of each sequence has no next member.')
(forall (s last)
(if
("sequence has last member" s last)
(not (exists (m)
("member is next after thing in sequence" m last s) ))))
(cl:comment 'Each member that participates in a unique sequence and that has no next member in the unique sequence is the last member of the unique sequence.')
(forall (s m)
(if
(and
("sequence has member" s m)
(not (exists (nm)
("next member is next after thing in sequence" nm m s) )))
("sequence has last member" s m)))
(cl:comment 'thing is the member of exactly one sequence position in the unique sequence and previous member is the member of some sequence position of the unique sequence that is just before the sequence position of the thing')
(forall (s pm m)
(iff
("previous member is just before thing in unique sequence" pm m s)
(and
("unique sequence" s)
(exists (sp psp)
(and
("sequence has sequence position" s sp)
("sequence position has member" sp m)
("next sequence position succeeds sequence position" sp psp)
("sequence position has member" psp pm) )))))
(cl:comment 'The first member of each sequence has no previous member.')
(forall (s first)
(if
("sequence has first member" s first)
(not (exists (m)
("previous member is just before thing in sequence" m first s) ))))
(cl:comment 'Each member that participates in a unique sequence and that has no previous member in the unique sequence is the first member of the unique sequence.')
(forall (s m)
(if
(and
("sequence has member" s m)
(not (exists (nm)
("previous member is just before thing in sequence" nm m s) )))
("sequence has first member" s m)))
(cl:comment 'each element of the set is an instance of the concept')
(forall (s c) (iff
("set is of concept" s c)
(and
(set s) (concept c)
(forall (e)
(if ("set includes element" s e) (c e) ))
)))
(cl:comment 'set1 includes the thing and set1 includes each element of set2, and each element of set1 is the thing or an element of set2')
(forall (s1 s2 t) (iff
("set1 is set2 plus thing" s1 s2 t)
(and
(set s1) (set s2)
("thing is in set" t s1)
(forall (e)
(if ("thing is in set" e s2) ("thing is in set" e s2) ))
(forall (e)
(if ("thing is in set" e s1)
(or ("thing is in set" e s2) (= e t) ) ))
)))
(cl:comment 'set plus thing')
(forall (s1 s2 t) (iff
(= s1 ("set plus thing" s2 t))
("set1 is set2 plus thing" s1 s2 t) ))
(cl:comment '---------------End Sequences Vocabulary----------------------------')
)
(cl:text Quantities
(cl:comment 'Each quantity has exactly one quantity kind.')
(forall ((q quantity))
(exists ((qk "quantity kind"))
(and
("quantity has quantity kind" q qk)
(forall (qk2)
(if
("quantity has quantity kind" q qk2)
(= qk2 qk) )) )))
(cl:comment 'Each system of units is for exactly one system of quantities.')
(forall ((sou "system of units"))
(= (count
("system of units is for system of quantities" sou)) 1))
(cl:comment '---------------End Quantities Vocabulary----------------------------')
)
(cl:text MinimalMereology
(cl:comment 'Each part is part of itself.')
(forall (part)
("part of" part part))
(cl:comment 'If the part is part of the whole and the whole is part of the part then the part is the whole.')
(forall (part whole)
(if (and ("part of" part whole)
("part of" whole part))
(= part whole)))
(cl:comment 'If the part is part of some whole and the whole is part of some part3 then the part is part of part3.')
(forall (part whole part3)
(if (and ("part of" part whole)
("part of" whole part3))
("part of" part part3)))
(cl:comment 'There exists a thing that is part of thing1 and that is part of thing2.')
(forall (thing1 thing2)
(iff (overlaps thing1 thing2)
(exists (thing3)
(and
("part of" thing3 thing1)
("part of" thing3 thing2)))))
(cl:comment 'If a thing1 overlaps a thing2, then thing2 overlaps thing1.')
(forall (thing1 thing2)
(iff (overlaps thing1 thing2) (overlaps thing2 thing1) ))
(cl:comment 'the part is part of the whole and the whole is not part of the part')
(forall (part whole)
(iff ("proper part" part whole)
(and
("part of" part whole)
(not ("part of" whole part)))))
(cl:comment 'If a part1 is a proper part of a whole then there exists a part2 that is a proper part of the whole and that does not overlap part1.')
(forall (part1 whole)
(if ("proper part" part1 whole)
(exists (part2)
(and
("proper part" part2 whole)
(not (overlaps part2 part1)) ))))
(cl:comment '---------------End Minimal Mereology Vocabulary----------------------------')
)