Resolution (logic)

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; this method may prove the satisfiability of a first-order satisfiable formula, but not always, as it is the case for all methods for first-order logic[citation needed]. Resolution was introduced by John Alan Robinson in 1965.

Contents

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, ai is taken to be the complement to bj). The resulting clause contains all the literals that do not have complements. Formally:

\frac{
a_1 \lor \ldots \vee a_i \vee \ldots \lor a_n, 
\quad b_1 \lor \ldots \vee b_j \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 and bs are literals,
ai is the complement to bj, and
the dividing line stands for entails

The clause produced by the resolution rule is called the resolvent of the two input clauses.

When the two clauses contain more than one pair of complementary literals, the resolution rule can be applied (independently) for each such pair. However, only the pair of literals that are resolved upon can be removed: all other pairs of literals remain in the resolvent clause. Note that resolving any two clauses that can be resolved over more than one variable always results in a tautology.

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

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. The steps are as follows.

  • All sentences in the knowledge base and the negation of the sentence to be proved (the conjecture) are conjunctively connected.
  • The resulting sentence is transformed into a conjunctive normal form with the conjuncts viewed as elements in a set, S, of clauses.
    • For example  (A_1 \lor A_2) \land (B_1 \lor B_2 \lor B_3) \land (C_1) gives rise to the set S=\{A_1 \lor A_2, B_1 \lor B_2 \lor B_3, C_1\}.
  • The resolution rule is applied to all possible pairs of clauses that contain complementary literals. After each application of the resolution rule, the resulting sentence is simplified by removing repeated literals. If the sentence contains complementary literals, it is discarded (as a tautology). If not, and if it is not yet present in the clause set S, it is added to S, and is considered for further resolution inferences.
  • If after applying a resolution rule the empty clause is derived, the original formula is unsatisfiable (or contradictory), and hence it can be concluded that the initial conjecture follows from the axioms.
  • If, on the other hand, the empty clause cannot be derived, and the resolution rule cannot be applied to derive any more new clauses, the conjecture is not a theorem of the original knowledge base.

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 English: 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

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

  • Find two clauses containing the same predicate, where it is negated in one clause but not in the other.
  • Perform a unification on the two predicates. (If the unification fails, you made a bad choice of predicates. Go back to the previous step and try again.)
  • If any unbound variables which were bound in the unified predicates also occur in other predicates in the two clauses, replace them with their bound values (terms) there as well.
  • Discard the unified predicates, and combine the remaining ones from the two clauses into a new clause, also joined by the "∨" operator.

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

Xa

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, 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

References

External links


Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Resolution — may refer to: Resolution (audio), a measure of digital audio quality Resolution (logic), a rule of inference used for automated theorem proving Resolution (law), a written motion adopted by a deliberative body Resolution (debate), the statement… …   Wikipedia

  • Logic programming — is, in its broadest sense, the use of mathematical logic for computer programming. In this view of logic programming, which can be traced at least as far back as John McCarthy s [1958] advice taker proposal, logic is used as a purely declarative… …   Wikipedia

  • Logic and the philosophy of mathematics in the nineteenth century — John Stillwell INTRODUCTION In its history of over two thousand years, mathematics has seldom been disturbed by philosophical disputes. Ever since Plato, who is said to have put the slogan ‘Let no one who is not a geometer enter here’ over the… …   History of philosophy

  • Logic Quest 3D — is a computer game published in 1997 by The Learning Company. It is recommended for ages 8 to 14, and primarily builds thinking and problem solving skills. Minimum System Requirements [Broderbund Support Center] Windows: ** Pentium 60 MHz… …   Wikipedia

  • Resolution (Logik) — Die Resolution ist ein Verfahren der formalen Logik, um eine logische Formel auf Gültigkeit zu testen. Das Resolutionsverfahren, auch Resolutionskalkül genannt, ist ein Widerlegungsverfahren: Statt direkt die Allgemeingültigkeit einer Formel zu… …   Deutsch Wikipedia

  • Outline of logic — The following outline is provided as an overview of and topical guide to logic: Logic – formal science of using reason, considered a branch of both philosophy and mathematics. Logic investigates and classifies the structure of statements and… …   Wikipedia

  • First-order logic — is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic (a less… …   Wikipedia

  • SLD resolution — ( Selective Linear Definite clause resolution) is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses. The SLD inference ruleGiven a goal clause: eg L… …   Wikipedia

  • Règle de résolution — La règle de résolution ou principe de résolution de Robinson est une règle d inférence logique que l on peut voir comme une généralisation du modus ponens. Cette règle est principalement utilisée dans les systèmes de preuve automatiques, elle est …   Wikipédia en Français

  • Hegel’s logic and philosophy of mind — Willem deVries LOGIC AND MIND IN HEGEL’S PHILOSOPHY Hegel is above all a systematic philosopher. Awe inspiring in its scope, his philosophy left no subject untouched. Logic provides the central, unifying framework as well as the general… …   History of philosophy

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”