Resolution (logic) explained

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation-complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the (complement of the) Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.

The resolution rule can be traced back to Davis and Putnam (1960);[1] however, their algorithm required trying 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.

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,

lnotc

is taken to be the complement to

c

). The resulting clause contains all the literals that do not have complements.Formally:
a1\lora2\lor\lorc, b1\lorb2\lor\lor\negc
a1\lora2\lor\lorb1\lorb2\lor
where

all

ai

,

bi

, and

c

are literals,

the dividing line stands for "entails".

The above may also be written as:

(\nega1\land\nega2\land)c, c(b1\lorb2\lor)
(\nega1\land\nega2\land)(b1\lorb2\lor)

Or schematically as:

\Gamma1\cup\left\{\ell\right\

\Gamma2\cup\left\{\overline{\ell}\right\}}{\Gamma1\cup\Gamma2}|\ell|

We have the following terminology:

\Gamma1\cup\left\{\ell\right\}

and

\Gamma2\cup\left\{\overline{\ell}\right\}

are the inference's premises

\Gamma1\cup\Gamma2

(the resolvent of the premises) is its conclusion.

\ell

is the left resolved literal,

\overline{\ell}

is the right resolved literal,

|\ell|

is the resolved atom or pivot.

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.[2]

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).

pq,p
q
is equivalent to
lnotp\lorq,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.[3] The steps are as follows.

(A1\lorA2)\land(B1\lorB2\lorB3)\land(C1)

gives rise to the set

S=\{A1\lorA2,B1\lorB2\lorB3,C1\}

.

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

a\veeb,\nega\veec
b\veec

In plain language: Suppose

a

is false. In order for the premise

a\veeb

to be true,

b

must be true.Alternatively, suppose

a

is true. In order for the premise

\nega\veec

to be true,

c

must be true. Therefore, regardless of falsehood or veracity of

a

, if both premises hold, then the conclusion

b\veec

is true.

Resolution in first-order logic

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

\Gamma1\cup\left\{L1\right\

\Gamma2\cup\left\{L2\right\}}{(\Gamma1\cup\Gamma2)\phi}\phi

where

\phi

is a most general unifier of

L1

and

\overline{L2}

, and

\Gamma1

and

\Gamma2

have no common variables.

Example

The clauses

P(x),Q(x)

and

\negP(b)

can apply this rule with

[b/x]

as unifier.

Here x is a variable and b is a constant.

P(x),Q(x)\negP(b)
Q(b)

[b/x]

Here we see that

P(x),Q(x)

and

\negP(b)

are the inference's premises

Q(b)

(the resolvent of the premises) is its conclusion.

P(x)

is the left resolved literal,

\negP(b)

is the right resolved literal,

P

is the resolved atom or pivot.

[b/x]

is the most general unifier of the resolved literals.

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:

\forallx.P(x)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.

\negP(x)\veeQ(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)

Factoring

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,[5] in that a set of clauses is unsatisfiable if and only if there exists a derivation of the empty clause using only resolution, enhanced by factoring.

An example for an unsatisfiable clause set for which factoring is needed to derive the empty clause is:

\begin{array}{rlcl}(1):&P(u)&\lor&P(f(u))\(2):&lnotP(v)&\lor&P(f(w))\(3):&lnotP(x)&\lor&lnotP(f(x))\\end{array}

Since each clause consists of two literals, so does each possible resolvent. Therefore, by resolution without factoring, the empty clause can never be obtained.Using factoring, it can be obtained e.g. as follows:[6]

\begin{array}{rll}(4):&P(u)\lorP(f(w))&byresolving(1)and(2),withv=f(u)\(5):&P(f(w))&byfactoring(4),withu=f(w)\(6):&lnotP(f(f(w')))&byresolving(5)and(3),withw=w',x=f(w')\(7):&false&byresolving(5)and(6),withw=f(w')\\end{array}

Non-clausal resolution

Generalizations of the above resolution rule have been devised that do not require the originating formulas to be in clausal normal form.[7] [8] [9] [10] [11] [12]

These techniques are useful mainly in interactive theorem proving where it is important to preserve human readability of intermediate result formulas. Besides, they avoid combinatorial explosion during transformation to clause-form,[9] and sometimes save resolution steps.[12]

Non-clausal resolution in propositional logic

For propositional logic, Murray[8] and Manna and Waldinger[9] use the rule

\begin{array}{c}F[p]          G[p]\\hlineF[it{true}]\lorG[it{false}]\\end{array}

,where

p

denotes an arbitrary formula,

F[p]

denotes a formula containing

p

as a subformula, and

F[it{true}]

is built by replacing in

F[p]

every occurrence of

p

by

it{true}

; likewise for

G

.The resolvent

F[it{true}]\lorG[it{false}]

is intended to be simplified using rules like

q\landit{true}\impliesq

, etc.In order to prevent generating useless trivial resolvents, the rule shall be applied only when

p

has at least one "negative" and "positive"[13] occurrence in

F

and

G

, respectively. Murray has shown that this rule is complete if augmented by appropriate logical transformation rules.[9]

Traugott uses the rule

\begin{array}{c}F[p+,p-]        G[p]\\hlineF[G[it{true}],lnotG[it{false}]]\\end{array}

,where the exponents of

p

indicate the polarity of its occurrences. While

G[it{true}]

and

G[it{false}]

are built as before, the formula

F[G[it{true}],lnotG[it{false}]]

is obtained by replacing each positive and each negative occurrence of

p

in

F

with

G[it{true}]

and

G[it{false}]

, respectively. Similar to Murray's approach, appropriate simplifying transformations are to be applied to the resolvent. Traugott proved his rule to be complete, provided

\land,\lor,,lnot

are the only connectives used in formulas.[11]

Traugott's resolvent is stronger than Murray's.[11] Moreover, it does not introduce new binary junctors, thus avoiding a tendency towards clausal form in repeated resolution. However, formulas may grow longer when a small

p

is replaced multiple times with a larger

G[it{true}]

and/or

G[it{false}]

.[11]

Propositional non-clausal resolution example

As an example, starting from the user-given assumptions

\begin{array}{rccc}(1):&a&&b\landc\(2):&c&&d\(3):&b\landd&&e\(4):&lnot(a&&e)\\end{array}

the Murray rule can be used as follows to infer a contradiction:[14]

\begin{array}{rrclccl}(5):&(it{true}d)&\lor&(ab\landit{false})&\implies&d\lorlnota&from(2)and(1),withp=c\(6):&(b\landit{true}e)&\lor&(it{false}\lorlnota)&\implies&(be)\lorlnota&from(3)and(5),withp=d\(7):&((it{true}e)\lorlnota)&\lor&(ait{false}\landc)&\implies&e\lorlnota\lorlnota&from(6)and(1),withp=b\(8):&(e\lorlnotit{true}\lorlnotit{true})&\lor&lnot(it{false}e)&\implies&e&from(7)and(4),withp=a\(9):&lnot(ait{true})&\lor&it{false}&\implies&it{false}&from(4)and(8),withp=e\\end{array}

For the same purpose, the Traugott rule can be used as follows :[11]

\begin{array}{rcccl}(10):&ab\land(it{true}d)&\implies&ab\landd&from(1)and(2),withp=c\(11):&a(it{true}e)&\implies&ae&from(10)and(3),withp=(b\landd)\(12):&lnotit{true}&\implies&it{false}&from(11)and(4),withp=(ae)\\end{array}

From a comparison of both deductions, the following issues can be seen:

p=c

.

p

the non-atomic formula

ae

in step (12). Using Murray's rules, the semantically equivalent formula

e\lorlnota\lorlnota

was obtained as (7), however, it could not be used as

p

due to its syntactic form.

Non-clausal resolution in first-order logic

For first-order predicate logic, Murray's rule is generalized to allow distinct, but unifiable, subformulas

p1

and

p2

of

F

and

G

, respectively. If

\phi

is the most general unifier of

p1

and

p2

, then the generalized resolvent is

F\phi[it{true}]\lorG\phi[it{false}]

. While the rule remains sound if a more special substitution

\phi

is used, no such rule applications are needed to achieve completeness.

Traugott's rule is generalized to allow several pairwise distinct subformulas

p1,\ldots,pm

of

F

and

pm+1,\ldots,pn

of

G

, as long as

p1,\ldots,pn

have a common most general unifier, say

\phi

. The generalized resolvent is obtained after applying

\phi

to the parent formulas, thus making the propositional version applicable. Traugott's completeness proof relies on the assumption that this fully general rule is used;[11] it is not clear whether his rule would remain complete if restricted to

p1==pm

and

pm+1==pn

.[15]

Paramodulation

Paramodulation is a related technique for reasoning on sets of clauses where the predicate symbol is equality. It generates all "equal" versions of clauses, except reflexive identities. The paramodulation operation takes a positive from clause, which must contain an equality literal. It then searches an into clause with a subterm that unifies with one side of the equality. The subterm is then replaced by the other side of the equality. The general aim of paramodulation is to reduce the system to atoms, reducing the size of the terms when substituting.[16]

Implementations

See also

References

. Jean Gallier . Logic for Computer Science: Foundations of Automatic Theorem Proving . . 1986 .

Notes and References

  1. Martin . Davis . Hilary . Putnam. A Computing Procedure for Quantification Theory. J. ACM. 1960. 7. 3. 201–215. 10.1145/321033.321034. 31888376 . free. Here: p. 210, "III. Rule for Eliminating Atomic Formulas".
  2. D.E. Knuth, The Art of Computer Programming 4A: Combinatorial Algorithms, part 1, p. 539
  3. "Before applying the inference method itself, we transform the formulas to quantifier-free conjunctive normal form."
  4. Book: Enrique P. . Arís . Juan L. . González . Fernando M. . Rubio . [{{GBurl|pS_6oZVbY2cC|pg=PR5}} Lógica Computacional ]. 2005 . Ediciones Paraninfo, S.A. . 9788497321822 .
  5. Book: Stuart J. . Russell . Peter . Norvig. Artificial Intelligence: A Modern Approach. 2009. Prentice Hall. 3rd . 350 . 978-0-13-604259-4.
  6. Book: Duffy, David A. . Principles of Automated Theorem Proving . Wiley . 1991 . 978-0-471-92784-6 . See p. 77. The example here is slightly modified to demonstrate a not-trivial factoring substitution. For clarity, the factoring step, (5), is shown separately. In step (6), the fresh variable

    w'

    was introduced to enable unifiability of (5) and (6), needed for (7).
  7. Master's Thesis. D. . Wilkins. QUEST: A Non-Clausal Theorem Proving System. 1973. University of Essex.
  8. Neil V. . Murray. A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic. February 1979. 39 . Electrical Engineering and Computer Science, Syracuse University . (Cited from Manna, Waldinger, 1980 as: "A Proof Procedure for Non-Clausal First-Order Logic", 1978)
  9. Zohar Manna . Zohar . Manna . Richard Waldinger . Richard . Waldinger . A Deductive Approach to Program Synthesis. ACM Transactions on Programming Languages and Systems. January 1980. 2. 90–121. 10.1145/357084.357090. 14770735 .
  10. N.V. . Murray. Completely Non-Clausal Theorem Proving. Artificial Intelligence. 1982. 18. 67–85. 10.1016/0004-3702(82)90011-x.
  11. Book: Traugott, J. . Nested Resolution . https://doi.org/10.1007/3-540-16780-3_106 . 8th International Conference on Automated Deduction. CADE 1986 . 978-3-540-39861-5 . 394–403 . Springer . . 230 . 1986 . 10.1007/3-540-16780-3_106 .
  12. Schmerl . U.R.. Resolution on Formula-Trees. Acta Informatica. 1988. 25. 4 . 425–438. 10.1007/bf02737109. 32702782 . Summary
  13. These notions, called "polarities", refer to the number of explicit or implicit negations found above

    p

    . For example,

    p

    occurs positive in

    (p\landq)\lorr

    and in

    qp

    , negative in

    lnot(p\landq)\lorr

    and in

    pq

    , and in both polarities in

    p\leftrightarrowq

    .
  14. "

    \implies

    " is used to indicate simplification after resolution.
  15. Here, "

    =

    " denotes syntactical term equality modulo renaming
  16. Book: 7. Paramodulation-Based Theorem Proving . Robert. Nieuwenhuis. Alberto. Rubio. http://www.cmi.ac.in/~madhavan/courses/theorem-proving-2014/reading/Nieuwenhuis-Rubio.pdf . Alan J.A. . Robinson . Andrei . Voronkov . [{{GBurl|HxaWA4lep_kC|pg=PR9}} Handbook of Automated Reasoning ]. Elsevier . 2001 . 978-0-08-053279-0 . 371–444 .