Inference and Resolution

Inference

Database: a conjunction of formulas assumed to be true (axioms)
Databases containing contradictions
We would like to derive (prove) further formulas from the axioms using inference rules.
An inference procedure specifies how new formulas are to be derived and added to the database.
A sound inference procedure makes only valid conclusions.
A complete inference procedure makes all valid conclusions (proves all theorems). But it may be impossible to decide whether a formula or its negation is implied by a database. In this case the attempt to prove the formula may never terminate (semidecidability).
We would like an inference procedure which is at least sound and hopefully complete.

Given a conjunction of two disjunctions of literals (clauses), replace the original with a single disjunction (clause) after eliminating one pair consisting of a literal in one clause and its negation in the other clause. The new clause is the resolvent of the two clauses.

(p V q)
((~ p) V r)
-----------
(q V r)

Modus ponens as resolution

Contradiction (empty disjunction) as resolution

Resolution requires formulas to be translated to clause form, that is, a conjunction of disjunctions of literals (see how to do the conversion in the page on clause form)
Predicate logic
The two literals which are eliminated need not be identical if they contain variables. They need only unify with one another: constants must match exactly, variables must match under certain conditions (see the page on unification), the result of which is a set of variable bindings which is then propagated through the remaining literals in the resolvent.

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