Variation and Activity Axioms

Grammar Name: variation.bnf

Extension Name: variation.def

Grammars required by Process Descriptions: None

Process Descriptions

(uniform ?a)

< uniform_axiom > ::=	(forall (?s1 ?s2) 
				(iff	(do < term > ?s1 ?s2)
					< variation_formula >+))

(variegated ?a)

< variegated_axiom > ::=  (forall (?s ?s2 < variable >+) 
				(iff	(do ?a ?s1 ?s2)
					< occ_variation_formula >+))

Auxiliary Rules

< variation_formula > ::= 	(exists (< variable >*)
					(and	(subactivity < term > < term >)
						(do < term > ?s1 ?s2)))

< occ_variation_formula > ::= (if	  < successor_axiom >
				  	< variation_formula >)