Strong Poset Activity Axioms

Grammar Name: strongposets.bnf

Extension Name: strongposets.def

Grammars required by Process Descriptions: None

Process Descriptions

< strongposet_spec > ::= (and	(strong_poset ?occ)
				< soo_axiom >)

Auxiliary Rules

< tree_formula > ::= (exists (< variable >+)
			(and	(same_tree < variable > ?occ)
		  		(subactivity_occurrence < variable > < variable >)))

< precedes_formula > ::=	(soo_precedes < variable > < variable > < term >) |
                                (and < precedes_formula >+)

< parallel_formula > ::=	(parallel < variable > < variable > < term >) |
                                (and < precedes_formula >+)

< soo_axiom > ::=
(forall (?occ < variable >*)
	(if	  (exists (< variable >+)
			(and	< precedes_formula >*
				< parallel_formula >*
				< tree_formula >))))