ГОСТ Р ИСО 18629-43—2011
< strongposet
_
spec > ::= (and (strong
_
poset ?осс)
< soo
_
axiom >)
< tree
_
formula > ::= (exists (< variable >+)
(and (same
_
tree <variable > ?occ)
(subactivity
_
occurrence <variable > <variable >)))
< precedes
_
formula > ::= (soo
_
precedes < variable > < variable > < term >) |
(and <precedes
_
formula >+)
< parallel
_
formula > ::= (parallel < variable > < variable > <term >) |
(and <precedes
_
formula >+)
< soo
_
axiom > ::=
(forall (?occ< variable >*)
(implies (exists (< variable >+)
(and < precedes
_
formula >*
< paral!el
_
formula >*
<tree
_
formula >))))
7 Ограничения продолжительности событий
Данный раздел характеризует все определения, обусловленныеограничениями продолжительности
событий.
7.1 Примитивная лексика ограничений продолжительности событий
Л
ексика ограничений продолжительности событий не требует никаких примитивных соотношений.
7.2
Л
ексика ограничений продолжительности событий
В данном подразделе определены нижеследующие соотношения:
- (dur?осс);
- (delay ?осс1 ?осс2);
- (dur
_
equiv ?осс1 ?осс2);
- (delay
_
equiv?occ1 ?осс2);
- (constant ?а);
- (interval
_
duration ?а);
- (variable ?а).
Каждое понятиеопределяется неформальной семантикой иаксиомами KIF.
7.3 Теории ядра, обусловленные ограничениями продолжительности событий
Дляданныхдефинициоиальных расширений необходимы:
-duration.th;
- psl.
_
core.th.
7.4 Дефинициональные расширения, обусловленные ограничениями продолжительности
событий
Для ограничений продолжительности событий никакие дефинициональные расширения не тре
буются.
7.5 Определение ограничений продолжительности событий
Для ограничений продолжительности событий определены нижеследующие понятия.
7.5.1 dur
Функция «dur» задает продолжительностьмеждумоментом начала некоторогособытия и моментом
окончания некоторогособытия.
(forall (?осс)
(= (dur ?осс) (duration (beginof ?осс) (endof ?осс))))
7.5.2 delay
Функция «delay» задает продолжительность между моментом начала одного события и моментом
начала другого события.
8