ГОСТ Р ИСО 18629-41—2011
< rigid_spec > ::= (exists {< variable >*)
(and <occurrence_formula >
< branch_spec>))
< occurrence_disjunct > ::= < occurrencejiteral > |
(or <ocourrence_literal >*)
< occurronce_axiom > ::= (exists (< variable >*)
< occurrence_disjunct >)
8 Недетерминированные действия: структура ветвей и упорядочивание
Данный раздел характеризует все определения, обусловленные недетерминированными действия
ми: структура ветвей иупорядочивание.
8.1 Примитивная лексика структуры ветвей и упорядочивания
Лексика структуры ветвей иупорядочивания нетребует примитивных соотношений.
8.2 Определяемая лексика структуры вотвой и упорядочивания
В данном подразделе определены нижеследующие соотношения:
- (order_tree ?s1 ?s2 ?а):
- (root_automorphic ?осс1 ?осс2);
- (ordered ?осс);
- (nondet_ordered ?осс);
- (broken_ordered ?осс):
- (ordered ?осс).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
8.3 Теории, обусловленные структурой вотвей и упорядочиванием
Для данной теории необходимы:
- act_occ.th;
- complex.th:
- atomic.th;
- subactivity.th;
- occtree.th;
- psl_core.th.
8.4 Дефинициональные расширения, обусловленные структурой ветвей и упорядочива
нием
Для структуры ветвей иупорядочивания дефинициональные расширения нетребуются.
8.5 Определения структуры ветвей и упорядочивания
Для структуры ветвей иупорядочиванияопределены нижеследующие понятия.
8.5.1 Mono_treo
Указанное поддерево, имеющее корень в ?s1, может быть мономорфически встроено внутрь подде
рева. имеющего корень в ?s2.
(forall (?s1 ?s2 ?a) (iff(monojree ?s1 ?s2 ?a)
(forall (?s3 ?s4 ?s5)
(implies (and (min_precedes ?s1 ?s3 ?a)
(min_precedes ?s2 ?s4 ?a)
(mono ?s3 ?s4 ?a)
(min_precedes ?s3 ?s5 ?a))
(exists (?s6)
(and (mono ?s5 ?s6 ?a)
(min_precedes?s4 ?s6?a)))))))
8.5.2 Ordor_tree
Указанноесоотношение сохраняет значение, если существуетнекоторый автоморфизм порядка, ото
бражающий поддерево с корнем в ?s1 в поддерево с корнем в ?s2.
Ю