ГОСТ Р ИС0 18629-41—2011
(forall (?осс) (iff(folded ?осс)
(exists (?ocd)
(and (same_grovo ?ocd ?осс)
(forall (?осс2)
(implies (same_grove ?осс2 ?осс)
(branch_homomorphic ?осс1 ?осс2)))))))
7.5.3 Nondet_folded
Некоторое действие является недетерминированно сложенным тогда и только тогда, когдасуществу
ет ветвь такая, что наборсобытий на каждой ветви минимального деревадействий является перестановкой
набора событий на первой ветви.
(forall (?осс) (iff(nondet_fotded ?осс)
(forall (?ocd)
(implies (same_grove ?осс1 ?осс)
(exists (?осс2)
(and (same_grove ?осс2 ?осс)
(not(=?occ1 ?осс2))
(branch_homomorphic ?осс1 ?осс2)))))))
7.5.4 Partial_folded
Некотороедействие является частично сложенным тогда и только тогда, когда существует ветвь та
кая. что набор событий на каяедой ветви минимальногодеревадействий является перестановкой набора
событий на первой ветви.
(forall (?осс) (iff(partial_folded ?осс)
(exists (?осс1 ?осс2 ?оссЗ)
(and (same_grove ?осс1 ?осс)
(same_grove ?осс2 ?осс)
(not(= ?осс1 ?осс2))
(branch_homomorphic ?осс1 ?осс2)
(same_grove ?оссЗ ?осс)
(forall (?осс4)
(implies (and (same_grove ?осс4 ?осс)
(not (=?оссЗ ?осс4)))
(not (branchhomomorpbic ?оссЗ?осс4))))))))
7.5.5 Rigid
Некоторое действие является жестким тогда итолькотогда, когда ниодна из ветвей некоторого дере
ва действий не является гомоморфической.
(forall (?осс) (iff(rigid ?осс)
(forall (?осс1 ?осс2)
(implies (and (same_grove ?осс1 ?осс)
(same_grove ?осс2 ?осс)
(not (= ?осс1 ?осс2)))
(not (branch_homomorphic ?осс1 ?осс2))))))
7.6 Грамматика описаний процесса для складной структуры ветвей
Нижеследующие грамматические утверждения устанавливаютописания технологического процесса
ивспомогательные правила, определенные в KIFдля складной структуры ветвей.
< folded_spec > ::= (exists (< variable >)
(and (samejree < variable > ?occ)
< occurrence_axiom >))
< nondet_folded_spec > ::= (exists (<variable >)
(and (samejree < variable > ?occ)
(or <occurrence_axiom >*)))
< partial Jolded_spec > ::= (or < nondetJolded_spec >
< rigid_spec >)
9