ГОСТ Р ИСО 18629-13-2011
символ one означает константу, которая является мультипликативной
для функции mult.
7.5.9 Символ константы тах+
Неформальная семантика для символа константы тах+ такова:
тах+ —максимальный временной интервал.
7.5.10 Символ константы тах-
Неформальная семантика для символа константы max- такова:
max- —минимальный временной интервал.
7.6 Определения теории продолжительности операций
7.6.1 Определение 1
Функция time_add отображает временную точку ?П и временной
интервал ?d на временную точку ?t2 так, что временной интервал между ?П и
?t2 составляет ?d.
(forall (?И ?t2 ?d)
(iff (=?t2 (time_add ?П ?d))
(and (timepoint ?t1)
(timepoint ?t2)
(timeduration ?d)
(= ?d(duration ?t2 ?t1)))))
7.7 Аксиомы теории продолжительности операций
Ниже приведен полный набор аксиом для теории продолжительности
операций.
7.7.1 Аксиома 1
zero, max+ и max- —временные интервалы.
(and (timeduration zero)
(timeduration max+)
(timeduration max-))
7.7.2 Аксиома 2
Результат сложения двух временных интервалов также является
временным интервалом.
18