Preventable Precondition Axioms

Preventable Precondition Axioms

Grammar Name: preventable.bnf

Extension Name: preventable.def

Grammars required by Process Descriptions: occ_precond.bnf, state_precond.bnf

Process Descriptions

(preventable ?a)
< preventable_precond > ::=   
(forall (?s)
        ({if | iff} (and   (occurrence ?s < term >)
                                (legal ?s)
				(ubiquitous < term > < term >)
				< simple_state_axiom >)
                         {< leaf_constrained_axiom > | < inner_constrained_axiom}))
(possibly_preventable ?a)
< possibly_preventable_precond > ::=   
(forall (?s)
        ({if | iff} (and   (occurrence ?s < term >)
                                (legal ?s)
				(ubiquitous < term > < term >)
				< state_axiom >)
                         {< leaf_constrained_axiom > | < inner_constrained_axiom}))