ГОСТ Р ИСО 18629-13-2011
Константа max- меньше любого временного интервала, а константа тах+
больше любого временного интервала.
(forall (?d)
(implies (timeduration ?d)
(and (lesser ?d max+)
(lesser max- ?d))))
7.7.15 Аксиома 15
Результат сложения любого временного интервала (отличного от
константы тах+) с константой max- равен константе max-, и наоборот; а сумма
констант max- и тах+ равна нулю.
(forall (?d)
(implies (timeduration ?d)
(and (implies(not (=?d max-)) (= max+ (add ?d max+)))
(implies (not (=?d max+)) (=max- (add ?dmax-)))
(=zero (add max+ max-)))))
7.7.16 Аксиома 16
Функция продолжительности операции присваивает временной интервал
каждой паре временных точек.
(forall (?t1 ?t2)
(implies (and (timepoint ?t1)
(timepoint ?t2))
(timeduration (duration ?t1 ?t2))))
7.7.17 Аксиома 17
Каждыйвременнойинтервалравензначениюфункции
продолжительности операции для любой пары временных точек.
(forall (?d)
(implies (timeduration ?d)
(exists (?t1 ?t2)
(and (timepoint ?t1)
(timepoint ?t2)
(=?d (duration ?t1 ?t2))))))
7.7.18 Аксиома 18
Значение функции продолжительности операции равно нулю тогда и
только тогда, когда две временные точки совпадают.
(forall (?И ?t2)
(implies (and (timepoint ?t1)
(timepoint ?t2))
(iff (=zero (duration ?t1 ?t2))
(= ?t1 ?t2)))
21