ГОСТ Р ИС0 18629-41—2011
(implies (and (same_grove?occ1 ?осс)
(same_grove ?осс2 ?осс))
(branch_automorphic ?осс1 ?осс2))))))
6.5.4 Nondet_permuted
Событиеявляется недетерминированно перестановочным тогда и толькотогда, когда набор событий
на каждой ветви минимальногодерева действий является перестановкой набора событий на некоторых
других ветвях.
(foratl (?осс) (iff(nondet_permuted ?осс)
(forall (?ocd)
(implies (same_grove ?осс1 ?осс)
(exists (?осс2)
(and (same_grove ?ocd ?осс2)
(not(= ?осс1 ?осс2))
(branch_automorphic?осс1 ?осс2)))))))
6.5.5 Partial_pormuted
Событиеявляется частично перестановочнымтогда итолькотогда, когда существует ветвь, для кото
рой наборсобытий является перестановкой набора событий на некоторыхдругих ветвях. При этом суще
ствует ветвь, не являющаяся перестановкой какой-либодругой ветви.
(forall (?осс) (iff(partial_permuted ?осс)
(exist (?осс1 ?осс2 ?оссЗ)
(and (same_grove ?осс1 ?осс)
(same_grove?осс2 ?осс)
(not (= ?осс1 ?осс2))
(branch_automorphic ?осс1 ?осс2)
(same_grove?оссЗ ?осс)
(forall (?осс4)
(implies (and (same_grove ?оссЗ ?осс4 ?а)
(branch_automorpbic ?оссЗ ?осс4))
(=?оссЗ?осс4))))))))
6.5.6 Simple
Событие являетсяпростым тогдаитолько тогда,когда ниоднаизветвей какого-либо дерева действий
не является автоморфической.
(forall (?осс) (iff(simple ?осс)
(forall (?осс1 ?осс2)
(implies (and (same_grove ?ocd ?осс)
(same_grove ?осс2 ?осс)
(branch_automorphic ?осс1 ?осс2))
(=?осс1 ?осс2)))))
6.6 Грамматика соотношений перестановочной структуры ветвей
Нижеследующие грамматическиеутверждения устанавливаютописания технологического процесса
ивспомогательные правила, определенные в KIFдля перестановочной структуры ветвей.
П р и м е ч а н и е — Назначение и важность использования грамматических утверждений ИСО 18629
поясняется в ИСО 18629-1:2004 (пункты 3.3.8, 4.2.4 и 5.1).
< permuted_spec > ::= (forall (< variable >)
(implies (samejree <variable > ?occ)
<occurrence_sentence >))
<nondet_permuted_spec > ::= (forall (<variable >*)
(implies (samejree < variable > ?occ)
(or <occurrence_sentence >*)))
< partial_permuted_spec > ::= (or<nondet_permuted_spec >
< simple_spec >)
< simple_spec > ::= (exists (< variable >*)
(and <occurrenceJormula >
< brancb_spec >))
7