ГОСТ Р ИСО 18629-12—2010
- holds;
-prior.
8.3 Связь с другими наборами аксиом
В теории ядрадискретного состояния используются следующие теории:
- pslcore.th, установленная в ИСО 18629-11,
- occtree.th (теория ядра дерева случаев).
Лексикадефиницийдля теории ядра дискретного состояния нетребуется.
8.4 Неформальная семантика
8.4.1 Отношение state
Обозначение KIF символа state:
(state ?f)
Неформальная семантика символа state.
(state?f) принимает значение TRUE в интерпретации теории ядра дискретногосостояния тольков том
случае, если ?fпредставляет собой множество состояний ракурса рассмотрения интерпретации. Состояния
образуют подкатегориюобъекта.
П р и м е ч а н и е — Объект определен в ИСО 18629-11.
Состояния представляют те свойства иотношения в домене, которые могут изменяться в результате
произошедших случаевдеятельности.
8.4.2 Отношение holds
Обозначение KIFсимвола отношения holds:
(holds ?f ?осс)
Неформальная семантика символа отношения holds:
(holds ?f ?осс) принимает значение TRUE в интерпретации теории ядра дискретногосостояния только
в том случае, если состояние ?fявляется истинным после случая деятельности ?осс.
8.4.3 Отношение prior
Обозначение KIF символа отношения:
(prior ?f?осс)
Неформальная семантика для отношения prior.
(prior?f?осс) принимает значениеTRUE в интерпретации теории ядра дискретного состояния только в
том случае, если состояние ?fявляется истинным до случаядеятельности ?осс.
8.5 Аксиомы
Теория ядра дискретного состояния включает в себя следующие аксиомы.
8.5.1 Аксиома 1
Состояния являются объектами:
(forall(?f)
(implies (state ?f)
(object ?f)))
8.5.2 Аксиома 2
Отношение holds действует только междусостояниями ислучаями деятельности. Это означает, что
состояние является истинным послеслучаядеятельности ?о:
(forall (?f ?осс)
(implies (holds ?f?occ)
(and (state ?f)
(activity_occurrence ?occ))))
8.5.3 Аксиома 3
Отношение prior действует только между состояниями и случаями деятельности. Это означает, что
состояние является истинным послеслучаядеятельности ?о:
(forall (?f?occ)
(implies (prior ?f?occ)
(and (state ?f)
(activity_occurrer>ce ?occ))))
12