ГОСТ Р ИСО 18629-12—2010
(root ?осс2 ?а)
(or (and (initial ?осс1)
(initial ?осс2))
(exists (?осс4 ?а1 ?а2)
(and (= ?ocd (successor ?а1 ?occ4))
{= ?occ2 (successor ?a2 ?occ4)))))))))
10.6 Аксиомы
Теория ядра составной деятельности включает в себя следующие аксиомы.
10.6.1 Аксиома 1
Любые случаи деятельности на дереве деятельности соответствуют случаяматомарной деятель
ности. подчиненной этой деятельности:
(forall (?а ?осс1 ?осс2)
(implies(min_precedes ?осс1 ?осс2 ?а)
(exists (?а1 ?ар)
(and (subactivity ?а1 ?a)
(atomic?ap)
(subactivity ?a1 ?ap)
(occurrence_of ?occ2 ?ap)))))
10.6.2 Аксиома 2
Любыеслучаи деятельности надереве деятельности соответствуют случаям атомарной деятельнос
ти, подчиненной этойдеятельности:
(forall (?а ?осс1 ?осс2)
(implies (min_precedes ?осс1 ?осс2 ?а)
(exists (?а2 ?ар)
(and (subactivity ?а2 ?а)
(atomic?ар)
(subactivity ?а2 ?ар)
(occurrenco_of?occ1 ?ар)))))
10.6.3 Аксиома 3
Случаи корневогоэлемента на дереведеятельности соответствуют случаям атомарной деятельнос
ти. подчиненной этойдеятельности:
(forall (?а?осс1)
(implies (root ?осс1 ?а)
(exists(?а2 ?ар)
(and (subactivity ?а2 ?а)
(atomic ?ар)
(subactivity ?а2 ?ар)
(occurrence_of?occ1 ?ар)))))
10.6.4 Аксиома 4
На всех деревьяхдеятельности существует случай корневой подчиненной деятельности:
(forall (?осс1 ?осс2 ?а)
(implies (min_precedes ?осс1 ?осс2 ?а)
(exists (?оссЗ)
(and (root ?оссЗ ?а)
(or (min_precedes ?оссЗ?осс1 ?а)
(=?оссЗ?осс1))))))
10.6.5 Аксиома 5
Ниодин случай подчиненной деятельности надереве деятельности не может произойти раньшеслу
чая корневой подчиненной деятельности:
(forall (?осс ?а)
(implies (root ?осс ?а)
(not(exists (?осс2)
(min_precedes ?осс2 ?осс ?а)))))
18