Resolution (logic)

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation theorem-proving technique for sentences in propositional logic and first-order logic. In other words, iteratively applying the resolution rule in a suitable way allows for telling whether a propositional formula is satisfiable and for proving that a first-order formula is unsatisfiable. Attempting to prove a satisfiable first-order formula as unsatisfiable may result in a nonterminating computation; this problem doesn't occur in propositional logic.

The resolution rule can be traced back to Davis and Putnam (1960);[1] however, their algorithm required to try all ground instances of the given formula. This source of combinatorial explosion was eliminated in 1965 by John Alan Robinson's syntactical unification algorithm, which allowed one to instantiate the formula during the proof "on demand" just as far as needed to keep refutation completeness.[2]

The clause produced by a resolution rule is sometimes called a resolvent.

Resolution in propositional logic

Resolution rule

The resolution rule in propositional logic is a single valid inference rule that produces a new clause implied by two clauses containing complementary literals. A literal is a propositional variable or the negation of a propositional variable. Two literals are said to be complements if one is the negation of the other (in the following, \lnot c is taken to be the complement to c). The resulting clause contains all the literals that do not have complements. Formally:

\frac{
a_1 \lor \ldots \vee a_{i-1} \lor c \lor a_{i+1} \vee \ldots \lor a_n,
\quad b_1 \lor \ldots \vee b_{j-1} \lor \lnot c \lor b_{j+1} \vee \ldots \lor b_m}
{a_1 \lor \ldots \lor a_{i-1} \lor a_{i+1} \lor \ldots \lor a_n  \lor  b_1 \lor \ldots \lor b_{j-1} \lor b_{j+1} \lor \ldots \lor b_m}

where

all as, bs and c are literals,
the dividing line stands for entails

The clause produced by the resolution rule is called the resolvent of the two input clauses. It is the principle of consensus applied to clauses rather than terms.[3]

When the two clauses contain more than one pair of complementary literals, the resolution rule can be applied (independently) for each such pair; however, the result is always a tautology.

Modus ponens can be seen as a special case of resolution (of a one-literal clause and a two-literal clause).

\frac{
p \rightarrow q, p}
{
q
}

is equivalent to

\frac{
\lnot p \lor q, p}
{
q
}

A resolution technique

When coupled with a complete search algorithm, the resolution rule yields a sound and complete algorithm for deciding the satisfiability of a propositional formula, and, by extension, the validity of a sentence under a set of axioms.

This resolution technique uses proof by contradiction and is based on the fact that any sentence in propositional logic can be transformed into an equivalent sentence in conjunctive normal form.[4] The steps are as follows.

One instance of this algorithm is the original Davis–Putnam algorithm that was later refined into the DPLL algorithm that removed the need for explicit representation of the resolvents.

This description of the resolution technique uses a set S as the underlying data-structure to represent resolution derivations. Lists, Trees and Directed Acyclic Graphs are other possible and common alternatives. Tree representations are more faithful to the fact that the resolution rule is binary. Together with a sequent notation for clauses, a tree representation also makes it clear to see how the resolution rule is related to a special case of the cut-rule, restricted to atomic cut-formulas. However, tree representations are not as compact as set or list representations, because they explicitly show redundant subderivations of clauses that are used more than once in the derivation of the empty clause. Graph representations can be as compact in the number of clauses as list representations and they also store structural information regarding which clauses were resolved to derive each resolvent.

A simple example


\frac{a \vee b, \quad \neg a \vee c}
{b \vee c}

In plain language: Suppose a is false. In order for the premise a \vee b to be true, b must be true. Alternatively, suppose a is true. In order for the premise \neg a \vee c to be true, c must be true. Therefore regardless of falsehood or veracity of a, if both premises hold, then the conclusion b \vee c is true.

Resolution in first order logic

Resolution rule can be generalized to first-order logic to:[5]


\frac{\Gamma_1 \cup\left\{ L_1\right\} \,\,\,\, \Gamma_2 \cup\left\{ L_2\right\} }{ (\Gamma_1 \cup \Gamma_2)\phi } \phi

where \phi is a most general unifier of L_1 and \overline{L_2} and \Gamma_1 and \Gamma_2 have no common variables.

Example

The clauses P(x),Q(x) and \neg P(b) can apply this rule with [b/x] as unifier.

Here x is a variable and b is a constant.


\frac{P(x),Q(x) \,\,\,\, \neg P(b)}
{Q(b)}[b/x]

Here we see that

Informal explanation

In first order logic, resolution condenses the traditional syllogisms of logical inference down to a single rule.

To understand how resolution works, consider the following example syllogism of term logic:

All Greeks are Europeans.
Homer is a Greek.
Therefore, Homer is a European.

Or, more generally:

\forall x. P(x) \Rightarrow Q(x)
P(a)
Therefore, Q(a)

To recast the reasoning using the resolution technique, first the clauses must be converted to conjunctive normal form (CNF). In this form, all quantification becomes implicit: universal quantifiers on variables (X, Y, ...) are simply omitted as understood, while existentially-quantified variables are replaced by Skolem functions.

\neg P(x) \vee Q(x)
P(a)
Therefore, Q(a)

So the question is, how does the resolution technique derive the last clause from the first two? The rule is simple:

To apply this rule to the above example, we find the predicate P occurs in negated form

¬P(X)

in the first clause, and in non-negated form

P(a)

in the second clause. X is an unbound variable, while a is a bound value (term). Unifying the two produces the substitution

X a

Discarding the unified predicates, and applying this substitution to the remaining predicates (just Q(X), in this case), produces the conclusion:

Q(a)

For another example, consider the syllogistic form

All Cretans are islanders.
All islanders are liars.
Therefore all Cretans are liars.

Or more generally,

X P(X) → Q(X)
X Q(X) → R(X)
Therefore, ∀X P(X) → R(X)

In CNF, the antecedents become:

¬P(X) ∨ Q(X)
¬Q(Y) ∨ R(Y)

(Note that the variable in the second clause was renamed to make it clear that variables in different clauses are distinct.)

Now, unifying Q(X) in the first clause with ¬Q(Y) in the second clause means that X and Y become the same variable anyway. Substituting this into the remaining clauses and combining them gives the conclusion:

¬P(X) ∨ R(X)

The resolution rule, as defined by Robinson, also incorporated factoring, which unifies two literals in the same clause, before or during the application of resolution as defined above. The resulting inference rule is refutation-complete,[6] in that a set of clauses is unsatisfiable if and only if there exists a derivation of the empty clause using resolution alone.

Implementations

See also

Notes

  1. Martin Davis, Hilary Putnam (1960). "A Computing Procedure for Quantification Theory". J.ACM 7 (3): 201–215. doi:10.1145/321033.321034. Here: p.210, "III. Rule for Eliminating Atomic Formulas".
  2. J.A. Robinson (Jan 1965). "A Machine-Oriented Logic Based on the Resolution Principle". Journal of the ACM 12 (1): 23–41. doi:10.1145/321250.321253.
  3. D.E. Knuth, The Art of Computer Programming 4A: Combinatorial Algorithms, part 1, p. 539
  4. 1 2 Leitsch, Alexander (1997), The resolution calculus, EATCS Monographs in Theoretical Computer Science, Springer, p. 11, Before applying the inference method itself, we transform the formulas to quantifier-free conjunctive normal form.
  5. Enrique P. Arís, Juan L. González y Fernando M. Rubio, Lógica Computacional, Thomson, (2005).
  6. Stuart J. Russell; Peter Norvig (2009). Artificial Intelligence: A Modern Approach (3rd ed.). Prentice Hall. p. 350 (=p.286 in the 1st edition of 1995)

References

Approaches to non-clausal resolution, i.e. resolution of first-order formulas that need not be in clausal normal form, are presented in:

External links

This article is issued from Wikipedia - version of the Friday, March 18, 2016. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.