ГОСТ Р ИСО 18629-12—2010
11.6.4 Аксиома 4
Разные случаи деятельности соответствуют разным ветвям дерева деятельности:
(forall (?а ?s1 ?осс1 ?осс2)
(implies (and (occurrence_of ?ocd ?а)
(occurrence_of ?осс2 ?а)
(not (= ?осс 1 ?осс2))
(subactivity_occurrence ?s1 ?ocd)
(subactivity_occurrence ?s1 ?осс2))
(exists (?s2)
(and (min_precedes ?s1 ?s2 ?a)
(subactivity_occurrence?s1 ?occ1)
(not (subactivity_occurrence ?s 1?occ2))))))
11.6.5 Аксиома 5
Все случаи атомарной подчиненной деятельности случая составной деятельности являютсяэлемен
тами одной итой же ветви деревадеятельности:
(forall (?а ?а1 ?а2 ?осс ?s1 ?s2)
(implies (and (occurrence_of ?occ ?a)
(occurrence_of ?s1 ?a1)
(atomic?a1)
(occurrence_of ?s2?a2)
(atomic?a2)
(subactivity_occurrence ?s1 ?occ)
(subactivity_occurrence ?s2 ?occ))
(or (minprecedes ?s1 ?s2 ?a)
(min_precedes ?s2 ?s1 ?a)
(= ?s1 ?s2))))
11.6.6 Аксиома 6
Все элементы одной ветви дерева деятельности являются случаями атомарной подчиненнойдея
тельности однихи тех же случаев деятельности:
(forall (?а ?s1 ?s2 ?осс)
(implies (and (min_precedes ?s1 ?s2 ?a)
(subactivity_ooccurrence ?s2?occ))
(subactivity ..occurrence ?s1 ?occ))
11.6.7 Аксиома 7
Отношениеsubactivity_occurrence непротиворечит отношению subactivity:
(forall (?a1 ?a2 ?occ1 ?occ2)
(implies (and (occurrence_of ?occ1 ?a1)
(occurrence_of ?occ2 ?a2)
(subactivity„occurrence ?occ1 ?occ2))
(subactivity ?a1 ?a2)))
11.6.8 Аксиома 8
Отношение subactivity_occurrence является транзитивным:
(forall (?occ1 ?occ2 ?occ3)
(implies (and (subactivity_occurrence ?occ1 ?occ2)
(subactivity„occurrence ?occ2 ?occ3))
(subactivity_occurrence ?occ1 ?occ3)))
11.6.9 Аксиома 9
Случаи подчиненных деятельностей являются случаями одной подчиненной деятельности, если они
удовлетворяют условию включения ветви:
(forall (?а1 ?а2 ?осс1 ?осс2)
(implies (and (occurrence_of ?ocd ?а1)
(occurrence_of ?occ2?a2)
(subactivity?a1 ?a2)
(not (subactivity_occurrence ?occ 1?occ2)))
(exists (?s)
(and (subactivity „occurrence ?s ?occ2)
(not (subactivity_occurrence ?s?occ1))))))
23