ГОСТ Р ИС0 18629-41—2011
11.1 Примитивная лексика уплотняющей структуры ветвей
Лексика уплотняющей структуры ветвей нетребует примитивных соотношений.
11.2 Определяемая лексика уплотняющей структуры ветвей
Вданном подразделе определены нижеследующие соотношения:
- (compacted ?а);
- (nondet_compacted ?а);
- (partial_compacted ?а);
- (stiff?а).
Каждое понятиеопределяется неформальной семантикой и аксиомой KIF.
11.3 Теории, обусловленные уплотняющей структурой ветвей
Дляданной теории необходимы:
- act_occ.th;
- complex.th;
- atomic.th;
- subactivity.th:
- occtree.th;
- psl_core.th.
11.4 Дефинициональные расширения, обусловленные уплотняющей структурой ветвей
Дляданных расширений необходима перестановочная структура ветвей.
11.5 Определения уплотняющей структуры ветвей
Для уплотняющей структуры ветвей определены нижеследующие понятия.
11.5.1 Compacted
Некотороедействие является уплотненным тогда и толькотогда, когда существует ветвь такая, что
наборсобытий на каждой ветвиминимального дерева действий является перестановкой наборасобытий на
егопервой ветви.
(forall (?а) (iff(compacted ?а)
(exists (?ocd)
(and (occurrence_of ?ocd ?а)
(forall (?осс2)
(implies (and (occurrence_of ?осс2 ?a)
(not (same_grove ?occ1 ?occ2)))
(brancti_homomorphic ?occ1 ?occ2))))))))
11.5.2 Nondet_compacted
Некотороедействие является недетерминированно уплотненным тогда итолько тогда, когда суще
ствует ветвьтакая, чтонаборсобытий накаждой ветви минимальногодерева действий является переста
новкой набора событий наего первой ветви.
(forall (?а) (iff(nondet_compacted ?а)
(forall (?ocd)
(implies (ocajrrence_of?осс1 ?а)
(exists (?осс2)
(and (occurrence_of ?осс2 ?а)
(not(same_grove?occ1 ?осс2))
(branch_homomorphic?осс1 ?осс2)))))))
11.5.3 Partial_compacted
Некоторое действие является частично уплотненным тогда и только тогда, когда существует ветвь
такая, что набор событий на некоторой ветви (но не на всех) минимального дерева действий является
перестановкой набора событий на его первой ветви.
(forall (?а) (iff(partial_compacted ?а)
(exists (?осс1 ?осс2 ?оссЗ)
(and (occurrence_of ?осс1 ?а)
(occurrence_of ?осс2?а)
17