Automated Reasoning and Theorem Proving

Resolution is a single inference rule that operates on clauses — disjunctions of literals — and works as follows: given two clauses that each contain a literal and its complement (one has P, the other has ¬P), the resolution rule combines them into a new clause, the resolvent, that contains everything from both original clauses except the complementary pair. Resolution refutation uses this one rule to prove that a knowledge base KB entails a sentence α by instead showing that KB together with the negation of α, ¬α, is unsatisfiable — that no model can make them all true simultaneously. Concretely, everything is converted into clausal form, ¬α is added to the clause set, and resolution is applied repeatedly to the growing set of clauses; if the search eventually derives the empty clause, a clause with no literals at all, that is a direct witness of a logical contradiction, and the refutation is complete.

Resolution's importance rests on a completeness guarantee: refutation resolution is refutation-complete for first-order logic, meaning that whenever a set of clauses genuinely is unsatisfiable, resolution is guaranteed to eventually derive the empty clause from it. J.A. Robinson's 1965 paper is the origin of this result for first-order logic — it combined the propositional resolution rule, already known to be complete for ground clauses, with a unification algorithm that lets literals containing variables be matched under a substitution before they are resolved. That combination is what makes a single mechanical rule sufficient for full first-order reasoning rather than only for ground, variable-free sentences, replacing what had previously been a patchwork of specialized inference rules tailored to particular sentence forms. Because first-order entailment is only semi-decidable, this completeness guarantee is necessarily one-sided: resolution is guaranteed to find a refutation whenever one exists, but if the clause set is in fact satisfiable, the search may run forever without ever confirming that no contradiction can be derived.

Before resolution can be applied, a knowledge base must be converted into a uniform clausal normal form: implications are rewritten using negation and disjunction, negations are pushed inward past quantifiers using De Morgan-style transformations, existentially quantified variables are eliminated by Skolemization (replacing each with a new function of the universally quantified variables that scope over it), universal quantifiers are dropped once every remaining variable is implicitly understood to be universally quantified, and the resulting sentences are distributed into a conjunction of disjunctions of literals. This conversion is entirely mechanical and can be applied to any first-order knowledge base, however it was originally written by a human author, which is exactly what allows a single inference rule to replace what would otherwise be a large collection of ad hoc, sentence-shape-specific rules. That uniformity is a considerable practical simplification for anyone building a theorem prover, since the prover's search procedure only ever has to reason about one kind of object, a clause, rather than about the open-ended variety of sentence forms a knowledge engineer might originally have written.

Unification is the process of finding a substitution θ that makes two logical expressions syntactically identical. Given the sentences Knows(John,x) and Knows(John,Jane), for instance, the substitution θ={x/Jane} unifies them, since applying θ to the first sentence produces exactly the second. The unification algorithm works recursively: it compares the two expressions piece by piece — matching predicate or function symbols against each other, and matching argument lists position by position — and whenever it finds a variable aligned against a term, it extends the substitution being built to bind that variable to that term, then continues comparing the rest of the structure under the extended substitution. The algorithm fails only if it ever finds a mismatch that no substitution could repair, such as two different constant symbols aligned against each other, or two complex terms built from different function symbols. This same recursive matching procedure is what resolution relies on at every step to decide whether two literals from different clauses can be treated as complementary once their variables are appropriately instantiated.

Two expressions can often be unified in more than one way, but among all their unifiers there is always a single most general unifier, or MGU, unique up to renaming of variables, which places fewer restrictions on the variables involved than any other unifier does. For example, the substitution {y/John, x/z} is more general than {y/John, x/John, z/John}, because the first leaves z free to be anything while the second pins every variable down to a specific constant, John, that may not have been necessary to assume. Using the MGU rather than an arbitrary unifier matters in practice: because it commits to the least amount of information necessary to make the match, it keeps the resulting resolvent as widely applicable as possible for later steps in the proof, whereas a needlessly specific unifier can accidentally rule out proof paths that would otherwise have succeeded, by baking in a commitment the proof never actually required.

One subtlety in implementing unification is the occurs check: before binding a variable to a term, a correct unification algorithm should verify that the variable does not itself appear inside that term, since binding x to a term containing x, such as trying to unify x with Father(x), would create a circular, effectively infinite structure that no finite substitution could ever fully resolve. Many practical systems, including standard Prolog implementations, skip the occurs check for the sake of speed, since checking it at every step adds a traversal cost to what is otherwise a fast, purely structural comparison. This accepts a small risk of unsound results — a query might succeed on a circular structure that a fully correct unifier would have rejected — in exchange for substantially faster unification on the large majority of cases where the circularity never actually arises in practice. It is a pragmatic engineering tradeoff worth knowing about, precisely because it departs from the fully general, provably sound algorithm that theoretical treatments of resolution assume.

A definite clause is a disjunction of literals with exactly one positive literal, typically written as an implication whose conclusion is a single atomic sentence, such as (Fever(x)∧StiffNeck(x))⇒TestForMeningitis(x). Generalized Modus Ponens raises ordinary Modus Ponens from propositional to first-order logic: given atomic premises that unify, under some substitution θ, with the premises of such a rule, the rule's conclusion follows under that same substitution. Forward chaining applies this rule in the forward direction: it starts from the atomic sentences already in the knowledge base and repeatedly fires any rule whose premises are already satisfied, adding each newly derived atomic sentence back into the knowledge base, until no further inferences can be made. This strategy is data-driven — it is well suited to situations where the system needs to know everything that follows from a fixed body of facts, since it derives all of it in one systematic sweep.

Backward chaining instead works backward from a specific goal: to prove a query, it looks for rules whose conclusion matches the query, then recursively tries to prove each of that rule's premises as a new subgoal, using depth-first search through the space of subgoals until it either finds a chain of already-known facts that supports the original query or exhausts the possibilities and fails. Along the way, unification is used to match the query and subgoals against rule conclusions and known facts that may themselves contain variables, so the same substitution machinery from resolution reappears here in a more restricted, more efficient setting. This strategy is goal-driven and is well suited to answering one targeted question without wasting effort deriving facts that have nothing to do with it; it is also the mechanism underlying Prolog's SLD-resolution execution model and the "backward" consultation style of classic rule-based expert systems, where a user's single query drives the entire inference process rather than triggering a sweep over the whole knowledge base.

Both forward and backward chaining are sound and complete for knowledge bases restricted to definite clauses, but they are not free alternatives to full resolution — that completeness guarantee depends specifically on the restriction to definite clauses, which cannot express arbitrary negation or disjunction the way general clausal form can, so any domain that genuinely needs those features has to fall back on general resolution. Which of the two chaining strategies is more efficient in a given case depends on the branching factor and structure of the rule set: forward chaining can waste time deriving many facts irrelevant to any particular question a user might eventually ask, since it does not know in advance which of the facts it derives will turn out to matter, while naive backward chaining can recompute the same subgoal repeatedly across different branches of its search tree, redoing identical work every time that subgoal happens to reappear. This is why practical implementations often add memoization of already-solved subgoals — caching each subgoal's result the first time it is solved — specifically to avoid that redundant recomputation.