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