Appendix D: Reference Grammars

This is Appendix D of the Semantic Web Services Ontology (SWSO) document.

AtomicProcess Precondition Axioms

If an occurrence of an activity is legal (i.e., if its preconditions are met) then it implies that a particular condition must be true in the situation prior to that activity occuring. That condition is known as a precondition.

< atomic_process_precond > ::= 
forall ?s (occurrence(?s,< term >) and legal(?s)) ==> < simple_state_axiom >)))
< simple_state_axiom > ::=  
      ({forall | exists} < variable >*) < simple_state_formula >)
< simple_state_formula > ::=
          < simple_state_literal > |
          (not < simple_state_formula >) |
          (< simple_state_formula > and < simple_state_formula >)* |
          (< simple_state_formula > or < simple_state_formula >)* |
          (==> < simple_state_formula >) |
          (<==> < simple_state_formula >) 
< simple_state_literal > ::=    prior(< term  >,?s)

AtomicProcess Effect Axiom

If a certain condition holds in a situation and an activity occurs in that situation, then another condition will hold in the resulting situation. The condition that holds in the resulting situation is known as an effect of the activity occurrence.

< atomic_process_effect > ::=  
          forall ?s (occurrence(?s,<term >) and < simple_state_axiom >) ==> < simple_holds_axiom >))
< simple_holds_axiom > ::=  
          ({forall | exists} < variable >*) < simple_holds_formula >) 
< simple_holds_formula > ::=    
          < simple_holds_literal > | 
          (not < simple_holds_formula >) | 
          < simple_holds_formula >) and < simple_holds_formula >) |
          (< simple_holds_formula > or < simple_holds_formula >) | 
          (< simple_holds_formula > <==> < simple_holds_formula >) |
          (< simple_holds_formula > <==> < simple_holds_formula >)
< simple_holds_literal > ::= holds(< term >,?s)

AtomicProcess Input Axioms, i.e., Knowledge Precondition Axioms over inputs

Note that these have the same form as the AtomicProcess Precondition Axioms except that the condition that must hold is a formula involving Kref (Know the value of) fluents.

< atomic_process_k_precond > ::= 
         forall ?s (occurrence(?s,< term >) and legal(?s)) < ==> simple_kref_axiom >))) 
< simple_kref_axiom > ::=  
         ({forall | exists} < variable >*) < simple_kref_formula >)
< simple_kref_formula > ::=  
         < simple_kref_literal > | 
         (not < simple_kref_formula >) | 
         (simple_kref_formula > and < simple_kref_formula >) | 
         (simple_kref_formula > or < simple_kref_formula >) |
         (< simple_kref_formula > ==> < simple_kref_formula >) |
         (< simple_kref_formula > <==> < simple_kref_formula & gt;) 
< simple_kref_literal > ::=    prior(kref(< term  >,?s)

AtomicProcess Output Axioms, i.e., Knowlege Effect Axioms over outputs

Note that these have the same form as the AtomicProcess Effect Axioms except that the condition that must hold after occurrence of the activity is a formula involving Kref (Know the value of) fluents.

< atomic_process_k_effect > ::=  
          forall ?s (occurrence(?s,<term >) and < simple_state_axiom >) ==> < simple_kref_axiom >
< simple_kref_axiom > ::=  
          ({forall | exists} < variable >*) < simple_kref_formula >)
< simple_kref_formula > ::=    
          < simple_kref_holds_literal > | 
          (not < simple_kref_formula >) | (< simple_kref_formula > and < simple_kref_formula >) | 
          (< simple_kref_formula > or < simple_kref_formula >) 
< simple_kref_holds_literal > ::= holds(kref(< term >,?s))

Split

< split_axiom > ::=
forall ?occ < variable >*
occurrence(?occ, < variable >) ==> (exists < variable >+
(< precedes_formula >* and
< parallel_formula >* and
subactivity_occurrence(< variable > < variable >)))

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

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

Sequence

< sequence_axiom > ::=
forall ?occ,< variable >*
occurrence_of(?occ, < variable > ==> (exists < variable >+
< precedes_formula > and < precedes_formula >* and
subactivity_occurrence(< variable > < variable >)))

Unordered

< unordered_axiom > ::=
forall ?occ,< variable >*)
occurrence_of(?occ, < variable > ==> (exists (< variable >+)
subactivity_occurrence(< variable > < variable > and subactivity_occurrence(< variable > < variable >*)))

Choice

< choice_axiom > ::=  forall < variable >*
(same_grove < variable > ?occ) ==>
(< occurrence_sentence > or < occurrence_sentence >*)))

< occurrence_literal > ::= occurrence_of(< variable > < term >)
| subactivity_occurrence(< variable >,< variable >)

< occurrence_formula > ::= < occurrence_literal > |
(< occurrence_literal > and < occurrence_literal >*)

< occurrence_sentence > ::= (exists (< variable >*)
< occurrence_formula >)

Conditional

< conditional_axiom > ::=   (< simple_state_axiom > ==> 
< variation_formula >)

Iterate

< iterate_axiom > ::= forall (< term >,?s1,?s2
                                do(< term >,?s1,?s2) <==>
                                        < rep_formula >))

< rep_formula > ::=  exists (< term >)
                        (subactivity(< term >,< term >) and
                                (forall ?s3
                                   (do(< term >,?s1,?s3) ==>
                                            (?s2 = ?s3) or
                                            do(< term >,?s3,?s2))

Repeat

< repeat_axiom > ::=   (< simple_state_axiom >
==> < iterate_axiom >)

OrderedActivity

< ordered_axiom > ::=    forall < variable >
                                (same_grove(< variable >,?occ) ==>
                                          < ordered_sentence >) |
                        forall < variable >
                                (same_grove(< variable >,?occ) ==>
                                          < ordered_formula >)

< ordered_literal > ::=   min_precedes(< variable >,< variable >,< term >) |
                          next_subocc(< variable >,< variable >,< term >)

< ordered_list > ::=      < ordered_literal > |
                          (< ordered_literal > and < ordered_literal >)*

< conditional_occurrence > ::=  (< occurrence_formula > ==>
                                          < ordered_list >)

< ordered_sentence > ::=        (exists ?occ,< variable >
                                        root_occ(< variable >,?occ) and
                                        < occurrence_disjunct > and
                                        < conditional_occurrence >)

< ordered_conjunct > ::=        < ordered_literal > |
                                (and < ordered_formula >*)

< ordered_formula > ::=         (exists ?occ,< variable >
                                        root_occ(< variable >,?occ)
                                        < occurrence_disjunct > and
                                        < ordered_conjunct >) |
                                (< ordered_formula > or < ordered_formula >)*

OccActivity

< occactivity_axiom > ::=   forall ?occ,< variable >
                                (same_grove(< variable >,?occ) ==>
                                          < occurrence_sentence >) |
			     forall ?occ,< variable >*
                                  same_grove(< variable >,?occ) ==>
                                  (< occurrence_sentence > or < occurrence_sentence >)*))

< occurrence_literal > ::=      occurrence_f(< variable >,< term >) |
                                subactivity_occurrence(< variable >,< variable >)

< occurrence_formula > ::=      < occurrence_literal > |
                                (< occurrence_literal > and < occurrence_literal >)*

< occurrence_sentence > ::=     (exists < variable >*
                                        < occurrence_formula >)

TriggeredActivity

< trigger_activity > ::=	forall ?s 
					(< simple_state_axiom > ==>
						  < distribution_formula >)
< distribution_formula > ::= 	exists ?occ
					(occurrence(?occ,?a) and
					root_occ(?s,?occ))