A Plan is a Proof in Sit Calc

Prove ∃ sequence of actions entails a Goal: ⊨ Ψ

(do (an (do an-1 (,....,a2(do(a1, S0))))))⊨ Ψ where
Legal(a1...an) ≡ Poss(a, s0) ∧.. ∧ Poss( an-1 (,....,a2(do(a1, S0))))

This can be done with an automated theorem prover that performs sound and complete proofs using predicate logic and unification.

Advantages: completely automatic and the result is a stong plan that meets all the properties.

Disadvantage: must be a completely-ordered (sequence) of actions so unsuitable for workflows.
SitCalc is a completely domain-independent approach in that the proofs cannot take advantage of heuristic knowledge, and so can be inefficient.
 And you have to write down all those pesky frame axioms.

©2012 Charles Petrie - permission to reproduce widely with attribution.