ГОСТР ИС0 18629-43—2011
16.3 Теории ядра, обусловленные эффектами действий, основанными на продолжительно
сти и времени
Дляданной теории необходимы:
- duration.th;
- disc
_
state.th:
- occtree.th;
- psl
_
cofe.th.
16.4 Дефинициональные расширения, обусловленные эффектами действий, основанными
на продолжительности и времени
Дляданного расширения необходимы нижеследующиедефинициональные расширения.
- actdur.def;
- effects.def;
- state
_
precond.def.
16.5 Определения эффектов действий, основанных на продолжительности и времени
Дляэффектов действий, основанных на продолжительности ивремени, определены нижеследующие
понятия.
16.5.1 maintain
_
effects
Некоторое действиеподдерживает эффект при условии: если когда-либо какие-либодва события со
гласованы попродолжительности исостоянию, тоони согласованы и поэффектам (то есть посостоянию,
сохраняющемуся после события).
(foral! (?а) (iff(maintain
_
effects ?а)
(forall (?s1 ?s2)
(implies (and (occurrence ?s1 ?a)
(occurrence ?s2 ?a)
(state
_
equiv?s1 ?s2)
(dur
_
equiv?s1 ?s2))
(effects
_
equiv?a ?s1 ?s2)))))
16.5.2 partial
_
maintain
Некоторое действие поддерживает эффект частично тогда итолькотогда, когда существуют сохра
няющие эффект автоморфизмы, сохраняющие как продолжительность, так исостояние.
(forall (?а) (iff(partial
_
maintain ?а)
(and (exists (?s1)
(forall (?s2)
(implies (and (occurrence ?s1 ?a)
(occurrence ?s2 ?a)
(state
_
equiv ?s1 ?s2)
(dur
_
equiv ?s1 ?s2))
(effects
_
equrv ?a ?s1 ?s2))))
(exists (?s3 ?s4)
(and (occurrence ?s3 ?a)
(occurrence ?s4 ?a)
(dur
_
equiv ?s3 ?s4)
(not (effects
_
equiv ?a ?s3?s4)))))))
16.5.3 nonmaintain
Некоторое действие не поддерживает эффект тогда и только тогда, когдасохраняющие эффект авто
морфизм продолжительности иавтоморфизм переменных величин являютсятривиальными.
(forall (?а) (iff(nonmaintain ?а)
(forall (?s1)
(implies (occurrence ?s1 ?a)
(exists (?s2)
(and (occurrence ?s2 ?a)
(dur
_
equiv ?s1 ?s2)
(not (effects
_
equiv ?a ?s1 ?s2))))))>)
23