ГОСТ Р ИСО 18629-12—2010
(forall (?осс1 ?осс2) (iff(equiv_occ ?осс1 ?осс2)
(exists (?а1 ?а2 ?аЗ)
(and (occurrence_of ?осс 1(солс?а1 ?а2))
(occurrence_of ?осс2 (сопс ?а1 ?аЗ)))))))
11.5.5 Опродолоние 4
(forall (?s1 ?s2 ?а) (iff(hom ?s1 ?s2 ?a)
(exists (?occ1 ?occ2)
(and (iso_occ ?s1 ?s2)
(subactivity_occurrence?s1 ?occ1)
(subactivity..occurrence?s2 ?occ2)
(occurrence_of?occ1 ?a)
(occurrence_of ?occ2 ?a)
(not(= ?occ1 ?occ2))))))
11.5.6 Олредолоние 5
Два случая деятельности принадлежат к одному множеству деревьев деятельности только в том
случае, если они имеют общий корневой случай:
(forall (?осс1 ?occ2)(iff(same_grove?occ1 ?осс2)
(exists(?а)
(and (occurrence_of?occ1 ?а)
(occurrence_of ?осс2 ?а)
(or (and (initial (root_occ ?occ1))
(initial (root_occ ?occ2)))
(exists (?s4 ?a1 ?a2)
(and (= (root_occ ?occ1)(successor?a1 ?s4))
(= (root_occ ?occ2) (successor ?a2 ?s4)))))))))
11.6 Аксиомы
Теория ядра случаевдеятельности включает в себяследующие аксиомы.
11.6.1 Аксиома 1
Для каждой ветвидеревадеятельности ?а существуетслучай деятельности ?а. Все случаи атомар
ной подчиненной деятельности на ветви являются случаями подчиненной деятельности, соответствующи
ми этому случаю ?а.
(forall (?а ?осс1 ?осс2)
(implies (min_precedes?occ1 ?осс2 ?а)
(exists (?осс)
(and (occurrence ?осс?а)
(subactivity_occurrence ?осс1 ?осс)
(subactivity_occurrence ?осс2 ?осс)))))
11.6.2 Аксиома 2
Для каждой ветви дерева деятельности ?а существует случай деятельности ?а. Корневой случай
подчиненной деятельности на ветви является случаем подчиненной деятельности, соответствующим слу
чаюдеятельности ?а:
(forall (?а ?s)
(implies (root ?s ?a)
(exists (?occ)
(occurrence_of ?occ?a)
(subactivity_occurrence ?s ?occ))))
11.6.3 Аксиома 3
Каждый случай деятельности ?авключает всебя случаи атомарной подчиненной деятельности, кото
рые являются элементамидеревадеятельности ?а:
(forall (?осс ?а)
(implies (exists ?s1 ?s2)
(and (subactivity_occurrence?s1 ?occ)
(subactivity_occurrence ?s2 ?occ)
(root ?s2 ?a)
(or (min_precedes ?s2 ?s1 ?a)
(=?s1 ?s2))))))
22