ГОСТ Р ИСО 18629-41—2011
(not (same_grove ?осс1 ?осс2))
(branch_homomorphic?осс1 ?осс2)
(occurrence_of ?оссЗ ?а)
(same_grove ?оссЗ?осс1)
(forall (?осс4)
(implies(and (occurrenceof?осс4 ?а)
(not(= ?осс2 ?осс4))
(same_grove?осс2 ?осс4))
(not (branch_homomorphic ?осс2 ?осс4))))))))
11.5.4 Stiff
Некоторое действие?а является несгибаемым тогда итолько тогда,когда ниоднаиз ветвейнекоторо
годеревадействийдля ?а не является эпиморфической для ветвей какого-либодругогодеревадействий
для ?а.
(forall (?а) (if(stiff ?а)
(forall (?осс1 ?осс2)
(implies(and (occurrence_of ?ocd ?а)
(occurrence_of ?осс2 ?а)
(not (same_grove ?осс1 ?осс2)))
(not (branch_homomorphic?occ1 ?осс2))))))
11.6 Грамматика уплотняющей структуры ветвей
Нижеследующие грамматические утверждения устанавливают описаниятехнологического процесса,
определенные в KIF для уплотняющей структуры ветвей.
< compacted_spec > ::= (forall (< variable >)
(implies (occurrence < variable > < term >)
(exists (<variable >)
(and (occurrence < variable > < term >)
<occurrence_ax»om >)))))
< nondet_compacted_spec > ::= (forall (<variable >)
(implies (occurrence < variable > < term
>)
(exists (<variable >)
(and (occurrence < vanable >
<
term >)
(or <occurrence_axiom >*))))))
< partial_compacted_spec > ::= (or < nondet_compacted_spec >
< stiff_spec >)
< stiff_spec > ::= (exists (< variable >*)
(and < occurrence_formula >
< branch_spec >))
12 Спектр действий: деревья действий и переупорядочивание
Данный раздел характеризует все определения, обусловленные спектром действий: деревья дей
ствий и переупорядочивание.
12.1 Примитивная лексика деревьев действий и переупорядочивания
Лексикадеревьевдействий ипереупорядочивания не требует примитивныхсоотношений.
12.2 Определяемая лексика деревьев действий и переупорядочивания
В данном подразделе определены нижеследующие соотношения:
- (treeordered ?а);
- (partialjreeordered ?а);
-(nondet_treeordered ?а);
- (scrambled ?а).
Каждоепонятие определяется неформальной семантикой и аксиомой KIF.
18