ГОСТ Р ИСО 18629-41—2011
(forall (?а) (iff(nondQt_reordered ?а)
(forall (?ocd)
(implies (occurrence_of?occ1 ?а)
(exists (?осс2)
(and (occurrence_of ?occ2 ?a)
(not (same_grove ?occ1 ?occ2))
(branch_automorphic ?occ1 ?occ2)))))))
10.5.3 Partial_reordered
Некотороедействие является частично переупорядоченным тогда и только тогда, когда существует
ветвьтакая, чтоеенабор событий является перестановкой набора событий на некоторой другой ветви. При
этом существует некоторая ветвь, не являющаяся перестановкой событий на какой-либодругой ветви,
(forall (?а) (iff(partial_reordered ?а)
(exist (?осс1 ?осс2 ?оссЗ)
(and (occurrence_of ?осс1 ?а)
(occurrence_of ?осс2 ?а)
(not (same_grove ?осс1 ?осс2))
(branch_automorphic?occ1 ?осс2)
(occurrence_of ?оссЗ ?а)
(same_grove ?осс1 ?оссЗ)
(forall (?осс4)
(implies (and (occurrence_of ?осс4 ?а)
(not (= ?осс2 ?осс4))
(same_grove ?осс2 ?осс4))
(not (branchautomorphic ?осс2?осс4))))))))
10.5.4 Unorderablo
Некоторое действие являетсянеупорядоченным тогда итолько тогда, когданиодна из ветвей некото
рого дерева действий не является автоморфической для какой-либо другой ветви на других деревьях
указанногоспектрадействий.
(forall (?а) (iff(unorderable ?а)
(forall (?осс1 ?осс2)
(implies (and (occurrence_of ?ocd ?а)
(occurrence_of ?осс2?а)
(not(same_grove?occ1 ?осс2)))
(not (brancfi_automorphic?осс1 ?осс2))))))
10.6 Грамматика описаний процесса для перестановочных деревьев действий
Нижеследующие грамматические утверждения устанавливают описания технологического процесса,
определенные в KIF для перестановочныхдеревьевдействий (аксиомы перестановочных действий для
ветвей).
< reordered_spec > ::=(forall (< variable >)
(implies (occurrence < variable > < term >)
< occurrence_sentence >))
<nondet_reordered_spec > ::= (forall (<variable >*)
(implies (occurrence < variable > < term >)
(or< occurrence_sentence >*)))
< partial_reordered_spec >::=(or < nondet_reordered_spec>
< nonorderable_spec >)
< nonorderable_spec > ::= (exists (< variable >*)
(and <occurrence_formu!a >
< branch_spec>))
11 Спектр действий: уплотняющая структура ветвей
Данный раздел характеризует все определения, обусловленные спектромдействий: уплотняющая
структура ветвей.
16