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

* 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)

* 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)

* 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)

* 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_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_axiom > ::=

forall ?occ,< variable >*

occurrence_of(?occ, < variable > ==> (exists < variable >+

< precedes_formula > and < precedes_formula >* and

subactivity_occurrence(< variable > < variable >)))

< unordered_axiom > ::=

forall ?occ,< variable >*)

occurrence_of(?occ, < variable > ==> (exists (< variable >+)

subactivity_occurrence(< variable > < variable > and subactivity_occurrence(< variable > < variable >*)))

< 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_axiom > ::= (< simple_state_axiom > ==>

< variation_formula >)

< 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_axiom > ::= (< simple_state_axiom >

==> < iterate_axiom >)

< 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_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 >)

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