Schedule Activity Axioms

Grammar Name: schedule.bnf

Extension Name: schedule.def

Grammars required by Process Descriptions: embedding.bnf, actdur.bnf

Process Descriptions

< schedule_axiom > ::=	(forall (?s ?occ < variable >*) 
				< schedule_formula >)

< partial_spread_axiom > ::=  (forall (?s ?occ < variable >+) 
				  < partial_schedule_sentence >))

Auxiliary Rules

< schedule_formula > ::=  ({if | and} < subocc_formula >
			   	 	   < delay_literal >) 

< schedule_axiom > ::=	< schedule_formula> |
			(and < schedule_axiom > < schedule_axiom >+)

< partial_schedule_formula > ::=  ({if | and} < subocc_formula >
				 	   	   < delay_interval_axiom >)

< partial_schedule_sentence > ::=	
	< partial_schedule_formula> |
	(and < partial_schedule_sentence > < partial_schedule_sentence >+)

Auxiliary Rules

< delay_literal > ::=        	(= (delay ?occ1 ?occ2) < term >)

< delay_interval_literal > ::=	(lesser (delay ?occ1 ?occ2) < term >) |
				(lesser < term > (delay ?occ1 ?occ2))

< delay_interval_axiom > ::=          < delay_interval_literal > |
                                (not < delay_interval_axiom >) |
                                ({and | or} < delay_interval_axiom >*) |
                                ({if | iff} < delay_interval_axiom >)