ГОСТ Р ИСО 18629-12—2010
9.2 Примитивные функции
Нелогическая лексика теории ядра атомарной деятельности включает в себя следующий символ
примитивной функции:
- сопс.
9.3 Связь с другими наборами аксиом
В теории ядра атомарной деятельности используютсяследующие теории:
-pslcore.th. установленная в ИСО 18629-11 (ядро PSL);
- occtree.th (теория ядрадерева случаев):
- subactivity.th (теория ядра подчиненной деятельности).
Лексикадефиницийдля теории ядра атомарной деятельности не требуется.
9.4 Неформальная семантика
9.4.1 Отношение atomic
Обозначение KIF символа отношенияatomic:
(atomic ?а)
Неформальная семантика символа отношения atomic:
(atomic ?а) принимает значение TRUE винтерпретации теории ядра атомарной деятельности только в
том случае, если ?а являетсялибо примитивной деятельностью, либо суперпозицией множества парал
лельныхпримитивных деятельностей.
9.4.2 Отношение сопс
Обозначение KIF символа отношения сопс:
(сопс?а1 ?а2)
Неформальнаясемантика символа отношения сопс:
(=?аЗ (сопс ?а1 ?а2)) принимает значение TRUE в интерпретации теории ядра атомарной деятельно
сти только в том случае, если ?аЗ является атомарной деятельностью, являющейся суперпозицией двух
параллельных атомарных деятельностей ?а1 и?а2.
9.5 Определения
Данная теория ядра не включает в себя определений.
9.6Аксиомы
Теория ядра атомарной деятельности включает в себя следующиеаксиомы.
9.6.1 Аксиома 1
Любая примитивная деятельностьявляется атомарной:
(foratl (?а)
(implies (primitive ?а)
(atomic ?а)))
9.6.2 Аксиома 2
Функция сопс является идемпотентной:
(forall (?а)
(= ?а (сопс ?а ?а)))
9.6.3 Аксиома 3
Функциясопс является коммутативной:
(forall (?а1 ?а2)
(= (сопс ?а1 ?а2) (сопс ?а2 ?а1)))
9.6.4 Аксиома 4
Функциясопс является ассоциативной:
(forall (?а1 ?а2 ?аЗ)
(= (сопс ?а1 (сопс ?а2 ?аЗ)) (сопс (сопс ?а1 ?а2) ?аЗ)))
9.6.5 Аксиома 5
Параллельная агрегация атомарной деятельности является атомарной деятельностью:
(forall (?а1 ?а2)
(iff(atomic (сопс?а1 ?а2))
(and (atomic ?а1)
(atomic ?a2))))
14