ГОСТ Р ИСО 18629-42—2011
- (possibly_preventable ?а);
- (unpreventable ?а).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
10.3 Теории, обусловленные предотвращаемыми условиями выполнения действий
Для данной теории необходимы:
- occtree.th;
- psl_core.th.
10.4 Дефинициональные расширения, обусловленные предотвращаемыми условиями
выполнения действий
Для данных расширений необходимы:
- occ_precond.def;
- state_precond.def;
- precond.def.
10.5 Определения предотвращаемых условий выполнения действий
Для предотвращаемых условий выполнения действий определены нижеследующие понятия.
10.5.1 preventable
Некоторое действие является предотвращаемым тогда и только тогда, когда допустимые события
зависят от переменных, сохраняющихсвое значение при выполнении другихдействий на дереве событий,
(forall (?а) (iff(preventable ?а)
(forall (?s1 ?s2)
(implies (and
(occurrence ?s1 ?a)
(occurrence ?s2 ?a)
(state_equiv ?s1 ?s2)
(tree_equiv ?s1 ?s2))
(legal_equiv ?s1 ?s2)))))
10.5.2 possibly_preventable
Некоторое действие является возможно предотвращаемым тогда и только тогда, когда допустимые
события зависят от переменных, сохраняющих свое значение при выполнении другихдействий на дереве
событий.
(forall (?а) (iff(possibly_preventable ?а)
(exists (?s1)
(and (occurrence ?s1 ?a)
(forall (?s2)
(implies (and
(occurrence ?s2 ?a)
(state_equiv ?s1 ?s2)
(tree_equiv ?s1 ?s2))
(legal_equiv ?s1 ?s2)))))))
10.5.3 unpreventable
Некоторое действие является мепредотвращаемым тогда и только тогда, когда не существует соотно
шения между действительным событием и переменной, сохраняющей свое значение при выполнении дру
гих действий.
(forall (?а) (iff(unpreventable ?а)
(forall (?s1)
(implies (occurrence ?s1 ?a)
(exists (?s2)
(and
(occurrence ?s2 ?a)
(state_equiv ?s1 ?s2)
(tree_equiv ?s1 ?s2)
(not (legal_equiv ?s1 ?s2))))))))
13