ГОСТР ИС0 18629-43—2011
(and (subactivity < term > < term >)
(forall (?s3)
(implies (do < term > ?s1 ?s3)
(or(= ?s2 ?s3)
(do < term > ?s3 ?s2))))))
< partial_rep_formula > ::= (exists (< term > ?s3)
(and (subactivity < term > < term >)
(do < term > ?s1 ?s3)
(or(= ?s2 ?s3)
(do < term > ?s3 ?s2))))
10 Спектр действий: перестановочные деревья действий
Данный раздел характеризует все определения, обусловленные спектром действий: перестановоч
ное дереводействий.
10.1 Примитивная лексика перестановочных деревьев действий
Лексика перестановочныхдеревьевдействий не требует примитивных соотношений.
10.2 Определяемые соотношения перестановочных деревьев действий
Вданном подразделе определены нижеследующие соотношения:
- (reordered ?а):
- (partial_reordered ?а),
- (nondet_roorder ?а);
- (nonorderable ?а).
Каждое понятиеопределяется неформальной семантикой и аксиомой KIF.
10.3 Теории, обусловленные перестановочными деревьями действий
Дляданной теории необходимы:
- act_occ.th;
- complex.th;
- atomic.th;
- subactivity.th:
- occtree.th;
- psl_core.th.
10.4 Дефинициональные расширения, обусловленные перестановочными деревьями дей
ствий
Дляданных расширений необходима перестановочная структура ветвей.
10.5 Определения перестановочных деревьев действий
Для перестановочных деревьевдействий определены нижеследующиепонятия.
10.5.1 Reordered
Некоторое действие является переупорядоченным тогда итолькотогда, когда набор событий на каж
дойветви одного минимального деревадействий является перестановкой наборасобытий на ветви другого
деревадействий для ?а.
(forall (?а) (iff(reordered ?а)
(forall (?осс1 ?осс2)
(implies (and (occurrence_of ?осс1 ?а)
(occurrence_of ?осс2 ?а))
(branch_autorrx^h»c?осс1 ?осс2)))))
10.5.2 Nondot_reordered
Некотороедействие является недетерминированно переупорядоченным тогда итолькотогда, когда
набор событий на каждой ветви одного минимальногодерева действийдля ?а является перестановкой
набора событий на некоторой ветви другого минимальногодеревадействийдля ?а.
15