Theorem Proving as Search

How Resolution Theorem Proving is Search

Problem state: particular state of database (set of clauses, including original axioms, goal, and resolvents).
Goal state
- For true-false questions, a state in which one clause is the empty clause.
- For information questions, a state in which one clause contains a single positive literal with answer as predicate.
Extending a state
- Given a database, pick resolvable pairs, resolve them, and add resolvents to database (yielding a new database for each different resolution)
- Because resolution is expensive, however, it is more efficient if we can wait until the goal? test to do it.
Normally the path to the goal is not relevant, so we can just keep track of states at the end of paths, that is, particular databases.

Resolution Strategies: Extending States

Resolution is complete: if a database is inconsistent (has a contradiction), there is a resolution deduction of the empty clause from it. Most (though not all) resolution strategies are also complete.

Unit-preference resolution: prefer to resolve pairs in which one clause has only one literal.

Set-of-support resolution: resolve only pairs in which one of the clauses is either the negated goal or a resolvent derived from the negated goal.

Directed resolution

The clauses are Horn clauses, clauses with at most one positive literal. (Without this constraint, directed resolution would not be complete.)
The clauses are arranged in a particular direction: either with the positive literal always first or always last.
Resolution is only permitted on the literals at the beginning of clauses.
With the positive literals at the ends of clauses, we get forward reasoning. One constrained way to perform forward reasoning (with or without a goal) is to take each of the rules in turn and for each, search for a way to satisfy the antecedents:

Each problem state consists of the antecedents left to satisfy along with the current substitution.
A goal state is reached when there are no more antecedents to satisfy. The consequent instantiated with the substitution is returned.
Extending a state involves finding all ways to satisfy the next antecedent using assertions in the database.

With the positive literals at the beginnings of clauses, we get backward reasoning. One constrained way to perform backward reasoning is to treat it as a search for a way to satisfy a set of goals, beginning with the initial goal:

Each problem state consists of the goals left to satisfy and the current substitution.
A goal state is reached when there are no more goals to satisfy. "Yes" or the top-level goal instantiated with the current substitution is returned.
Extending a state involves finding all ways to satisfy the next goal using assertions and rules in the database. (See Prolog page for details.)

Last updated: 14 February 1996
URL: http://www.indiana.edu/~gasser/Q351/rtp_search.html
Comments: gasser@salsa.indiana.edu
Copyright 1996, The Trustees of Indiana University