Lines of Proof as basis for (naïve) encodings
Loop from k=1, until a solution is found
- Set up k-length sequence of disjunctive actions (a1 V a2 V ….V an)
- In effect, a direct naïve refinement is used (monotonic, complete, but not progressive)
- Impose constraints, satisfaction of which ensures that some sub-sequence of the disjunctive sequence is a solution
- The constraints set up lines of proof
- State-space proofs
- Graphplan’s backward search can be thought of as setting up backward proof
- Causal proofs
- Convert the constraints into your
favorite combinatorial substrate
and solve
[Mali & Kambhampati, 1999]