Context-Free Effect Axioms

Grammar Name: effects.bnf

Extension Name: effects.def

Grammars required by Process Descriptions: state_effects.bnf

Process Descriptions

(context_free ?a)

< context_free_effect > ::=	(forall (?s) 
					(if	 (occurrence ?s )
						 < simple_holds_axiom >))

(null ?a)

< null_effect > ::=		(forall (?s) 
					(if	 (occurrence ?s )
						 (iff 	< simple_holds_axiom >
							< simple_state_axiom >)))

Auxiliary Rules

< simple_holds_literal > ::= 	(holds < term  > ?s)

< simple_holds_formula > ::=	< simple_holds_literal > |
				(not < simple_holds_formula >) |
				({and | or} < simple_holds_formula >*) | 
				({if | iff} < simple_holds_formula >) 

< simple_holds_axiom > ::=	({forall | exists} < variable >*) 
					< simple_holds_formula >)