ГОСТ Р ИСО 18629-41—2011
(forall (?а) (iff(scrambled ?а)
(forall (?осс1 ?осс2)
(implies (and (occurrence_of ?ocd ?а)
(occurrence_of ?осс2 ?а)
(not(same_grove?occ1 ?осс2)
(not (root_automorphic?осс1 ?осс2))))))
12.6 Грамматика деревьев действий и пероупорядочивания
Нижеследующие грамматические утверждения устанавливают описания технологического процесса,
определенные в KIFдлядеревьевдействий и переупорядочивания.
<treeordered_spec > ::= (forall (< vanable >)
(implies (occurrence < vanable > < term >)
<ordered_sentence >)) |
(forall (<variable >)
(implies (occurrence < variable > < term >)
<ordered_fbrmula >))
< nondet_treeordered_spec >(forall (<variable >)
(implies (occurrence < variable > < term >)
(or <ordored_sentence >*)))
< partial_treeordered_spec > ::= (forall (< variable >)
(implies (occurrence < variable > < term >)
(or {<ordered_sentence >* |
<orderedJist >*})))
< scrambled_spec > ::= (forall (< variable
>)
(implies (occurrence < variable > < term >)
(or <orderedjist >*)))
13 Спектр и включение поддерева
Данный раздел характеризует все определения, обусловленные спектром ивключением поддерева.
13.1 Примитивная лексика спектра и включения поддерева
Лексикаспектра и включения поддерева не требует примитивныхсоотношений.
13.2 Определяемая лексика спектра и включения поддерева
В данном подразделеопределены нижеследующие соотношения:
- (subtree_embed ?осс1 ?осс2 ?а).
- (multiple_outcome ?а);
- (weak_outcome?а);
- (nondet_outcome ?а);
- (immiscible ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
13.3 Теории, обусловленные спектром и включением поддерева
Для данной теории необходимы:
- act_occ.th;
- complox.th;
- atomic.th;
- subactivity.th:
- occtree.th;
- psl_core.th.
13.4 Дофинициональные расширения, обусловленные спектром и включением поддерева
Для спектра и включения поддеревадефинициональные расширения не требуются.
13.5 Определения спектра и включения поддерева
Для спектра и включенияподдерева определены нижеследующие понятия.
20