Distribution and Activity Axioms

Distribution and Activity Axioms

Grammar Name: distribution.bnf

Extension Name: distribution.def

Grammars required by Process Descriptions: precond.bnf

Process Descriptions

(universal ?a) 
< universal_axiom > ::=	(forall (?s) 
				(if	  (legal ?s)
					  < distribution_formula>))
(restricted ?a) 
< restricted_axiom > ::= (forall (?s) 
				(if	  < successor_axiom >
					  < distribution_formula>))

Auxiliary Rules 

< distribution_formula > ::= 	(exists (?occ)
					(and	(occurrence ?occ ?a)
						(root_occ ?s ?occ)))