ГОСТ Р ИСО 18629-43—2011
<ordered
_
sentence >)
<durationJiteral >))
<part»al
_
order
_
dur
_
spec > ::=
(forall (?occ)
(implies (and (occurrence ?occ < term >)
<ordered
_
formula >)
< durationjiteral >)) |
(forall (?occ)
(implies (and (occurrence ?occ < term >)
< ordered
_
sentence >)
< interval Jiteral >))
12 Упорядочивание и ограничения продолжительности встроенных
событий
Данный раздел характеризует все определения, обусловленные упорядочиванием иограничениями
продолжительности встроенных событий.
12.1 Примитивная лексика упорядочивания и ограничений продолжительности встроенных
событий
Л
ексика упорядочивания иограничений продолжительности встроенныхсобытий не требует никаких
примитивных соотношений.
12.2 Описываемая лексика упорядочивания и ограничений продолжительности встроенных
событий
В данном подразделе определены нижеследующие соотношения:
- (embed
_
duration ?а):
- (partial
_
embed
_
duration ?а):
- (nonembed
_
duration ?а).
Каждое понятие определяется неформальной семантикой и аксиомами KIF.
12.3 Теории ядра, обусловленные упорядочиванием и ограничениями продолжительности
встроенных событий
Дляданных теорий необходимы:
-duration.th;
- act
_
occ.th;
- complex.th;
- atomic.th;
- subactivity.th;
- occtree.th:
- psl
_
core.th.
12.4 Дефинициональныо расширения, обусловленные упорядочиванием и ограничениями
продолжительности встроенных событий
Для упорядочивания и ограничений продолжительности встроенныхсобытий необходимо иметь:
- permute.def.
12.5 Определения упорядочивания и ограничений продолжительности встроенных событий
Дляупорядочивания иограничений продолжительности встроенных событий определены нижеследу
ющие понятия.
12.5.1 ombed
_
duration
Некоторое действие имеет встроеннуюпродолжительность тогда итолько тогда, когда все ветви авто-
морфных событий этогожедерева имеют одинаковую продолжительность.
(forall (?а) (iff(embed
_
duration ?а)
(forall (?осс1 ?осс2)
16