ГОСТР ИСО 18629-43—2011
13.2 Описываемая лексика входных условий нарушения выполнения действий
В данном подразделе определены нижеследующие соотношения:
- (spoilage ?а),
- (possible
_
spoilage ?а);
- (nonspoilage ?а).
Каждое понятие определяется неформальной семантикой и аксиомами KIF.
13.3 Теории, обусловленные входными условиями нарушения выполнения действий
Дляданной теории необходимы:
- duration.th,
- occtree.th:
- psl
_
core.th.
13.4 Дсфинициональныс расширения, обусловленные входными условиями нарушения
выполнения действий
Для входных условий нарушения выполнениядействий необходимы нижеследующиедефиницио-
нальные расширения:
- occ
_
precond.def;
- time
_
precond.def;
- precond.def.
13.5 Определения входных условий нарушения выполнения действий
Для входныхусловий нарушения выполнениядействий определены нижеследующие понятия.
13.5.1 spoilage
Выполнение некоторогодействия нарушенотогда итолько тогда, когда допустимые события зависят
от задержки между другими событиями. В особенности это события, находящиеся как на одной орбите
эндоморфизмов дерева событий, так инаодной орбите автоморфизмовзадержки.
(forall (?а) (iff(spoilage ?а)
(forall (?s1 ?s2)
(implies (and (occurrence
_
of ?s1 ?a)
(occurrence
_
of ?s2 ?a)
(delay
_
equiv ?s1 ?s2)
(tree
_
equiv ?s1 ?s2))
(legal
_
equiv?s1 ?s2)))))
13.5.2 possible
_
spoilage
Выполнение некоторогодействия возможнонарушенотогда итолько тогда, когда существуют собы
тия. находящиеся как на одной орбите эндоморфизмов дерева событий, такинаодной орбите автоморфиз
мов задержки.
(forall (?а) (iff(possiblo
_
spoilage ?а)
(exists (?s1)
(and(occurrence
_
of?s1 ?a)
(forall (?s2)
(implies (and (occurrence
_
of ?s2 ?a)
(delay
_
equiv?s1 ?s2)
(tree
_
equiv?s1 ?s2))
(Iegal
_
equiv?s1 ?s2))))))
13.5.3 nonspoilago
Выполнение некоторогодействия не нарушенотогда и толькотогда, когда отсутствует связь между
допустимыми событиями и задержкой между другими событиями. При этом единственный эндоморфизм
дерева событий, сохраняющийзадержку между другими событиями, является тривиальным.
(forall (?а) (iff(nonspoilage ?а)
(forall (?s1)
(implies (occurrence
_
of ?s1 ?a)
(exists (?s2)
18