ГОСТ Р ИСО 18629-42—2011
6.6Грамматика соотношений для основанных на состоянии входных условий выполнения
действий
Нижеследующие грамматические утверждения устанавливают описания процессов и вспомогатель
ные правила, определенные в KIF для основанных на состоянии входных условий выполнения действий.
П р и м е ч а н и е — Функция и важность грамматических утверждений поясняются в ИСО 18629-1:2004
(подразделы 3.3.8. 4.2.4 и 5.1).
< simple_state_precond > ::= (forall (?s)
(implies (and (occurrence ?s)
(legal ?s))
< simple_state_axiom >))) |
(forall (?s)
(implies (and (legal ?s)
< simp!e_state_axiom >)
(legal (successor < term > ?s))))
< state_precond > ::= (forall (< variable >*)
(implies (and (occurrence < variable > < term >)
(legal < term >))
< state_axiom >))) |
(forall (< variable >*)
(implies (and (legal < term >)
< state_axk>m >)
(legal (successor < term > < term >))))
(prior < term > ?s)
< simple_state_literal > |
(not < simple_state_formula >) |
({and |or} < simple_state_formula >*) |
({implies | iff} < simple_state_formula >)
({forall | exists} < variable >*)
<simple_state_formula >)
(prior < term > < variable >)
< statejiteral > |
(not < state_formula >))
({and | or} < state_formula >) |
({implies | iff} < state_formula >*)
(forall (< variable >+) < state_formula >)
< simple_state_literal > ::=
< simpie_state_formula > ::=
< simple_state_axiom > ::=
< statejiteral > ::=
< state_formula > ::=
< state axiom > ::=
7 Временные входные условия выполнения действий
Данный раздел характеризует все определения, обусловленные временными входными условиями
выполнения действий. Критерий классификации указанныхдействий: зависит или нетдействительное вы
полнение некоторогодействия толькоот времени выполнения указанныхдействий.
7.1 Примитивная лексика временных входных условий выполнения действий
Лексика временных входных условий выполнения действий не требует примитивных отношений.
7.2 Описываемая лексика понятий для временных входныхусловийвыполнения
действий
В данном подразделе описываются нижеследующие отношения:
- (begin_equiv ?s1 ?s2),
- (time_precond ?a):
- (partialjime ?a);
- (rigidJime ?a).
Каждое понятие определяется неформальной семантикой и аксиомой KIF.
7