Proof As Search

Proof as Search: Up to now we have exhibited proofs as if they were found miraculously. We gave formulae and showed proofs of the intended results. We did not exhibit how the proofs were derived.
We now examine how proofs can actually be found. In so doing we stress the close ties between theorem proving and search.

A General Proof Procedure: We use binary resolution [we represent clauses as sets] and we represent the proof as a tree, the Proof Tree. In this tree nodes represent clauses. We start with two disjoint sets of clauses INITIAL and OTHERS.

We create a node START and introduce a hyperarc from START to new nodes, each representing a distinct element of INITIAL. We put in a set OPEN all these new nodes. These nodes are called AND Nodes.
If OPEN is empty, we terminate. Otherwise we remove an element N from OPEN using a selection function SELECT.
If N is an AND node, we connect N with a single hyperarc to new nodes N1 ... Nm, one for each literal in the clause C represented at N. These nodes are also labeled with C and are called OR Nodes. All of these nodes are placed into OPEN.
[NOTE 1: In the case that C consists of a single literal, we can just say that N is now an OR node.]
[NOTE 2: One may decide not to create all the nodes N1 .. Nm in a single action and instead to choose one of the literals of C and to create a node Ni to represent C with this choice of literal. Ni is inserted into OPEN. N also goes back into OPEN if not all of its literals have been considered. The rule used to choose the literal in C is called a Selection Rule]
Repeat from 2.
If N is an OR node, say, corresponding to the ith literal of a clause C, we consider all the possible ways of applying binary resolution between C and clauses from the set OTHERS, resolving on the ith literal of C.
Let D1 .. Dp be the resulting clauses. We represent each of these clauses Dj by an AND node N(Dj) as in 1. above. We put an arc from N to N(Dj). We set OPEN to NEXT-OPEN(OPEN, C, {D1, .., Dp}). We set OTHERS to NEXT-OTHERS(OTHERS, C, {D1, .., Dp}). If in the proof tree we have, starting at START, a hyperpath (i.e. a path that may include hyperarcs) whose leaves have all label {}, we terminate with success.

[NOTE 3: One may decide, instead of resolving C on its ith literal with all possible element of OTHERS, to select one compatible element of OTHERS and to resolve C with it, putting this resolvent and C back into OPEN. We would call a rule for selecting an element of OTHERS a Search Rule.]
Repeat from 2

In this proof procedure we have left indetermined:

The sets INITIAL and OTHERS of clauses
The function SELECT by which we choose which node to expand
The function NEXT-OPEN for computing the next value of OPEN
The function NEXT-OTHERS for computing the next value of OTHERS

There is no guaranty that for any choice of INITIAL, OTHERS, SELECT, NEXT-OPEN and NEXT-OTHERS the resulting theorem prover will be "complete", i.e. that everything that is provable will be provable with this theorem prover.

Example: Suppose that we want to prove that
1. NOT P(x) OR NOT R(x) is inconsistent with the set of clauses:
2. NOT S(x) OR H(x)
3. NOT S(x) OR R(x)
4. S(b)
5. P(b)

The following are possible selections for the indeterminates:
INITIAL: {1.}, that is, it consists of the clauses representing the negation of the goal.
OTHERS: {2. 3. 4. 5.}, that is, it consists of the non-logical axioms.
SELECT: We use OPEN as a FIFO queue, i.e. we do breadth-first search.
NEXT-OPEN: It sets NEXT-OPEN(OPEN, C, {D1, .., Dp}) to the union of OPEN, {C}, and {D1, .., Dp}.
NEXT-OTHERS: It leaves OTHERS unchanged

The Proof Tree is then (we underline AND nodes and all their outgoing arcs are assumed to form a single hyperlink)

At an OR node we apply resolution between the current clause at its selected literal and all the compatible elements of OTHERS.