Wed Sep 9 09:05:16 CEST 2009

Resolution (Logic)

Reading CTM[1] chapter 9 about relational + logic programming.

The basic idea is that you want theorem proving: given a logic
sentence, the system needs to find a proof for it.  On page 634 it

- theorem prover is limited (Goedel's [in]completeness theorems)
- algorithmic complexity: need a predictable operational semantics
- deduction should be constructive

This is ensured by restricting the form of axioms so that an efficient
constructive theorem prover is possible.  For Prolog these axioms are
Horn clauses, which allow an inference rule called resolution[2].
Additionally, Prolog allows to add hints to map a logic program to a
more efficient operational semantics.

[1] http://www.info.ucl.ac.be/~pvr/book.html
[2] http://en.wikipedia.org/wiki/Resolution_%28logic%29