{{Short description|Inference rule in logic, proof theory, and automated theorem proving}}
In [[mathematical logic]] and [[automated theorem proving]], '''resolution''' is a [[rule of inference]] leading to a [[Completeness (logic)#Refutation-completeness|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 [[RE (complexity)|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 [[Martin Davis (mathematician)|Davis]] and [[Hilary Putnam|Putnam]] (1960);<ref>{{cite journal| first1=Martin |last1=Davis |first2=Hilary |last2=Putnam| title=A Computing Procedure for Quantification Theory| journal=J. ACM| year=1960| volume=7| number=3| pages=201–215| doi=10.1145/321033.321034|s2cid=31888376 | doi-access=free}} Here: p. 210, "III. Rule for Eliminating Atomic Formulas".</ref> however, their [[Davis-Putnam algorithm|algorithm]] required trying all [[ground instance]]s of the given formula. This source of [[combinatorial explosion]] was eliminated in 1965 by [[John Alan Robinson]]'s syntactical [[Unification (computer science)|unification algorithm]], which allowed one to instantiate the formula during the proof "on demand" just as far as needed to keep [[refutation completeness]].<ref>{{harvnb|Robinson|1965}}</ref>
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 [[Clause (logic)|clauses]] containing complementary literals. A [[literal (mathematical logic)|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, <math>\lnot c</math> is taken to be the complement to <math>c</math>). The resulting clause contains all the literals that do not have complements. Formally: :<math>\frac{ a_1 \lor a_2 \lor \cdots \lor c, \quad b_1 \lor b_2 \lor \cdots \lor \neg c} {a_1 \lor a_2 \lor \cdots \lor b_1 \lor b_2 \lor \cdots}</math> where : all <math>a_i</math>, <math>b_i</math>, and <math>c</math> are literals, : the dividing line stands for "[[logical consequence|entails]]".
The above may also be written as: :<math>\frac{ (\neg a_1 \land \neg a_2 \land \cdots) \rightarrow c, \quad c \rightarrow (b_1 \lor b_2 \lor \cdots)} {(\neg a_1 \land \neg a_2 \land \cdots) \rightarrow (b_1 \lor b_2 \lor \cdots)}</math>
Or schematically as: :<math> \frac{\Gamma_1 \cup\left\{ \ell\right\} \,\,\,\, \Gamma_2 \cup\left\{ \overline{\ell}\right\} }{\Gamma_1 \cup\Gamma_2}|\ell| </math>
We have the following terminology: * The clauses <math>\Gamma_1 \cup\left\{ \ell\right\}</math> and <math>\Gamma_2 \cup\left\{ \overline{\ell}\right\} </math> are the inference's premises * <math>\Gamma_1 \cup \Gamma_2</math> (the resolvent of the premises) is its conclusion. * The literal <math>\ell</math> is the left resolved literal, * The literal <math>\overline{\ell}</math> is the right resolved literal, * <math>|\ell|</math> 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 theorem|consensus]]'' applied to clauses rather than terms.<ref>D.E. Knuth, ''[[The Art of Computer Programming]]'' '''4A''': ''Combinatorial Algorithms'', part 1, p. 539</ref>
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 (logic)|tautology]].
[[Modus ponens]] can be seen as a special case of resolution (of a one-literal clause and a two-literal clause). :<math>\frac{ p \rightarrow q, \quad p} { q }</math> is equivalent to :<math>\frac{ \lnot p \lor q,\quad p} { q }</math>
=== A resolution technique === When coupled with a complete [[search algorithm]], the resolution rule yields a [[Soundness|sound]] and [[Completeness (logic)|complete]] algorithm for deciding the ''satisfiability'' of a propositional formula, and, by extension, the [[Validity (logic)|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]].<ref name="leitsch">{{harvnb|Leitsch|1997|p=11}} "Before applying the inference method itself, we transform the formulas to quantifier-free conjunctive normal form."</ref> 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.<ref name="leitsch"/> **For example, <math> (A_1 \lor A_2) \land (B_1 \lor B_2 \lor B_3) \land (C_1)</math> gives rise to the set <math>S=\{A_1 \lor A_2, B_1 \lor B_2 \lor B_3, C_1\}</math>. * 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 clause 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 [[Logical consequence|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|data-structure]] to represent resolution derivations. [[List (data structure)|Lists]], [[Tree (data structure)|Trees]] and [[Directed Acyclic Graph]]s 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|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 ==== <math> \frac{a \vee b, \quad \neg a \vee c} {b \vee c} </math>
In plain language: Suppose <math>a</math> is false. In order for the premise <math>a \vee b</math> to be true, <math>b</math> must be true. Alternatively, suppose <math>a</math> is true. In order for the premise <math>\neg a \vee c</math> to be true, <math>c</math> must be true. Therefore, regardless of falsehood or veracity of <math>a</math>, if both premises hold, then the conclusion <math>b \vee c</math> is true.
== Resolution in first-order logic ==
Resolution rule can be generalized to [[first-order logic]] to:<ref>{{cite book |first1=Enrique P. |last1=Arís |first2=Juan L. |last2=González |first3=Fernando M. |last3=Rubio |title=Lógica Computacional |date=2005 |publisher=Ediciones Paraninfo, S.A. |isbn=9788497321822 |url={{GBurl|pS_6oZVbY2cC|pg=PR5}} }}</ref>
:<math> \frac{\Gamma_1 \cup\left\{ L_1\right\} \,\,\,\, \Gamma_2 \cup\left\{ L_2\right\} }{ (\Gamma_1 \cup \Gamma_2)\phi } \phi </math>
where <math>\phi</math> is a [[most general unifier]] of <math>L_1</math> and <math>\overline{L_2}</math>, and <math>\Gamma_1</math> and <math>\Gamma_2</math> have no common variables.
=== Example === The clauses <math>P(x),Q(x)</math> and <math>\neg P(b)</math> can apply this rule with <math>[b/x]</math> as unifier.
Here x is a variable and b is a constant.
:<math> \frac{P(x),Q(x) \,\,\,\, \neg P(b)} {Q(b)}[b/x] </math>
Here we see that
* The clauses <math>P(x),Q(x)</math> and <math> \neg P(b) </math> are the inference's premises * <math> Q(b) </math> (the resolvent of the premises) is its conclusion. * The literal <math>P(x)</math> is the left resolved literal, * The literal <math>\neg P(b)</math> is the right resolved literal, * <math>P</math> is the resolved atom or pivot. * <math>[b/x]</math> is the most general unifier of the resolved literals.
=== Informal explanation === In first-order logic, resolution condenses the traditional [[syllogism]]s of [[rule of inference|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:
: <math>\forall x. P(x) \Rightarrow Q(x)</math> : <math>P(a)</math> : Therefore, <math>Q(a)</math>
To recast the reasoning using the resolution technique, first the clauses must be converted to [[conjunctive normal form]] (CNF). In this form, all [[Quantification (logic)|quantification]] becomes implicit: [[Universal quantification|universal quantifiers]] on variables (''X'', ''Y'', ...) are simply omitted as understood, while [[Existential quantification|existentially-quantified]] variables are replaced by [[Skolem function]]s.
: <math>\neg P(x) \vee Q(x)</math> : <math>P(a)</math> : Therefore, <math>Q(a)</math>
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 (computing)|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
: ''X'' {{mapsto}} ''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'')
(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,<ref>{{cite book| first1=Stuart J. |last1=Russell |first2=Peter |last2=Norvig| title=Artificial Intelligence: A Modern Approach| year=2009| publisher=Prentice Hall|edition=3rd |page=350 |isbn=978-0-13-604259-4}}</ref> 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: :<math>\begin{array}{rlcl} (1): & P(u) & \lor & P(f(u)) \\ (2): & \lnot P(v) & \lor & P(f(w)) \\ (3): & \lnot P(x) & \lor & \lnot P(f(x)) \\ \end{array}</math> 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:<ref>{{cite book | first=David A. |last=Duffy | title=Principles of Automated Theorem Proving | publisher=Wiley | year=1991 |isbn=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]] <math>w'</math> was introduced to enable unifiability of (5) and (6), needed for (7).</ref> :<math>\begin{array}{rll} (4): & P(u) \lor P(f(w)) & \text{by resolving (1) and (2), with } v=f(u) \\ (5): & P(f(w)) & \text{by factoring (4), with } u=f(w) \\ (6): & \lnot P(f(f(w'))) & \text{by resolving (5) and (3), with } w=w', x=f(w') \\ (7): & \text{false} & \text{by resolving (5) and (6), with } w=f(w') \\ \end{array}</math>
==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]].<ref>{{cite thesis| type=Master's Thesis| first=D. |last=Wilkins| title=QUEST: A Non-Clausal Theorem Proving System| year=1973| publisher=University of Essex}}</ref><ref name="Murray.1979">{{cite tech report| first=Neil V. |last=Murray| title=A Proof Procedure for Quantifier-Free Non-Clausal First Order Logic|date=February 1979| number=39 |publisher=Electrical Engineering and Computer Science, Syracuse University |url=https://surface.syr.edu/eecs_techreports/39 }} (Cited from Manna, Waldinger, 1980 as: "A Proof Procedure for Non-Clausal First-Order Logic", 1978)</ref><ref name="Manna.Waldinger.1980">{{cite journal| author1-link=Zohar Manna |first1=Zohar |last1=Manna |author2-link=Richard Waldinger |first2=Richard |last2=Waldinger | title=A Deductive Approach to Program Synthesis| journal=[[ACM Transactions on Programming Languages and Systems]]|date=January 1980| volume=2| pages=90–121| doi=10.1145/357084.357090|s2cid=14770735 | url=https://apps.dtic.mil/sti/citations/ADA065558}}</ref><ref>{{cite journal| first=N.V. |last=Murray| title=Completely Non-Clausal Theorem Proving| journal=[[Artificial Intelligence (journal)|Artificial Intelligence]]| year=1982| volume=18| pages=67–85| doi=10.1016/0004-3702(82)90011-x}}</ref><ref name="Traugott.1986">{{cite book |first=J. |last=Traugott | chapter=Nested Resolution |chapter-url=https://doi.org/10.1007/3-540-16780-3_106 |title=8th International Conference on Automated Deduction. CADE 1986 |isbn=978-3-540-39861-5 |pages=394–403 | publisher=Springer | series=[[LNCS]] | volume=230 | year=1986 |doi=10.1007/3-540-16780-3_106 }}</ref><ref name="Schmerl.1988">{{cite journal| last=Schmerl |first=U.R.| title=Resolution on Formula-Trees| journal=[[Acta Informatica]]| year=1988| volume=25|issue=4 | pages=425–438| doi=10.1007/bf02737109|s2cid=32702782 }} [http://www.zentralblatt-math.org/ioport/en/?id=2297405&type=pdf Summary]</ref>
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,<ref name="Manna.Waldinger.1980"/>{{rp|98}} and sometimes save resolution steps.<ref name="Schmerl.1988"/>{{rp|425}}
===Non-clausal resolution in propositional logic=== For propositional logic, Murray<ref name="Murray.1979"/>{{rp|18}} and Manna and Waldinger<ref name="Manna.Waldinger.1980"/>{{rp|98}} use the rule
:<math>\begin{array}{c} F[p] \;\;\;\;\;\;\;\;\;\; G[p] \\ \hline F[\textit{true}] \lor G[\textit{false}] \\ \end{array}</math>,
where <math>p</math> denotes an arbitrary formula. Here <math>F[p]</math> and <math>G[p]</math> denote formulas containing <math>p</math> as a subformula. <math>F[\textit{true}]</math> is built by replacing every occurrence of <math>p</math> in <math>F[p]</math> by <math>\textit{true}</math>. Similarly, <math>G[\textit{false}]</math> is built by replacing every occurrence of <math>p</math> in <math>G[p]</math> by <math>\textit{false}</math>. The resolvent <math>F[\textit{true}] \lor G[\textit{false}]</math> is intended to be simplified using rules like <math>q \land \textit{true} \implies q</math>, etc. In order to prevent generating useless trivial resolvents, the rule is applied only when <math>p</math> has at least one "negative" and "positive"<ref>These notions, called "polarities", refer to the number of explicit or implicit negations found above <math>p</math>. For example, <math>p</math> occurs positive in <math>(p \land q) \lor r</math> and in <math>q \rightarrow p</math>, negative in <math>\lnot (p \land q) \lor r</math> and in <math>p \rightarrow q</math>, and in both polarities in <math>p \leftrightarrow q</math>.</ref> occurrence in <math>F</math> and <math>G</math>, respectively. Murray has shown that this rule is complete if augmented by appropriate logical transformation rules.<ref name="Manna.Waldinger.1980"/>{{rp|103}}
Traugott uses a rule that can be similarly expressed as :<math>\begin{array}{c} F[p^+,p^-] \;\;\;\;\;\;\;\; G[p] \\ \hline F[G[\textit{true}],\lnot G[\textit{false}]] \\ \end{array}</math>, where the exponents of <math>p</math> indicate the polarity of its occurrences. While <math>G[\textit{true}]</math> and <math>G[\textit{false}]</math> are built as before, the formula <math>F[G[\textit{true}],\lnot G[\textit{false}]]</math> is obtained by replacing each positive occurrence of <math>p</math> in <math>F</math> with <math>G[\textit{true}]</math> and each negative occurrence with <math>G[\textit{false}]</math>. Similar to Murray's approach, appropriate simplifying transformations are to be applied to the resolvent. Traugott proved his rule to be complete, provided <math>\land, \lor, \rightarrow, \lnot</math> are the only connectives used in formulas.<ref name="Traugott.1986"/>{{rp|398–400}}
Traugott's resolvent is stronger than Murray's.<ref name="Traugott.1986"/>{{rp|395}} 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 <math>p</math> is replaced multiple times with a larger <math>G[\textit{true}]</math> and/or <math>G[\textit{false}]</math>.<ref name="Traugott.1986"/>{{rp|398}} <!------------------------------------------------------------------- Schmerl's resolvent R satisfies R \implies F \lor G, rather than F \land G \implies R, see his Lemma 2, p. 432; omit his approach for now, since it is not easy to make it comparable to the previous ones------------------------------------------------- Schmerl uses the rule :<math>\begin{array}{c} F(p) \;\;\; G(p) \\ \hline F(G(\textit{true})) \\ \end{array}</math>, when <math>p</math> occurs with different polarities in <math>F</math> and <math>G</math>. Unlike the previous approaches, he replaces only a single occurrence of <math>p</math> by <math>\textit{true}</math> in <math>G</math>, and by <math>G(\textit{true})</math> in <math>F</math>.<ref name="Schmerl.1988"/>{{rp|429}} Moreover, he does not handle arbitrary formulas, but uses a special data structure, viz. an [[and-or tree]], with each leaf annotated with an atomic formula and its polarity; his replacement operation ignores the polarity of the replaced subtree. He proved his rule to be complete.<ref name="Schmerl.1988"/>{{rp|434}}
Schmerl's rule closely resembles a simplified version of Traugott's, for <math>p</math> occurring negative in <math>F</math> and positive in <math>G</math>, the former still yields <math>F(G(\textit{true}))</math> while the latter yields <math>F[,\lnot G[\textit{false}]]</math>.<ref name="Schmerl.1988"/>{{rp|435}} Schmerl's rule does not introduce any new junctors. In some cases, it was found to be stronger than that of Murray, however, no proof appears to exist that it cannot be weaker in some other cases. -------------------------------------------------------------------->
===Propositional non-clausal resolution example=== As an example, starting from the user-given assumptions :<math>\begin{array}{rccc} (1): & a & \rightarrow & b \land c \\ (2): & c & \rightarrow & d \\ (3): & b \land d &\rightarrow & e \\ (4): & \lnot (a & \rightarrow & e) \\ \end{array}</math> the Murray rule can be used as follows to infer a contradiction:<ref>"<math>\implies</math>" is used to indicate simplification after resolution.</ref> :<math>\begin{array}{rrclccl} (5): & (\textit{true} \rightarrow d) & \lor & (a \rightarrow b \land \textit{false}) & \implies & d \lor \lnot a & \mbox{from (2) and (1), with } p=c \\ (6): & (b \land \textit{true} \rightarrow e) & \lor & (\textit{false} \lor \lnot a) & \implies & (b \rightarrow e) \lor \lnot a & \mbox{from (3) and (5), with } p=d \\ (7): & ((\textit{true} \rightarrow e) \lor \lnot a) & \lor & (a \rightarrow \textit{false} \land c) & \implies & e \lor \lnot a \lor \lnot a & \mbox{from (6) and (1), with } p=b \\ (8): & (e \lor \lnot \textit{true} \lor \lnot \textit{true}) & \lor & \lnot (\textit{false} \rightarrow e) & \implies & e & \mbox{from (7) and (4), with } p=a \\ (9): & \lnot (a \rightarrow \textit{true}) & \lor & \textit{false} & \implies & \textit{false} & \mbox{from (4) and (8), with } p=e \\ \end{array}</math> For the same purpose, the Traugott rule can be used as follows :<ref name="Traugott.1986"/>{{rp|397}} :<math>\begin{array}{rcccl} (10): & a \rightarrow b \land (\textit{true} \rightarrow d) & \implies & a \rightarrow b \land d & \mbox{from (1) and (2), with } p=c \\ (11): & a \rightarrow (\textit{true} \rightarrow e) & \implies & a \rightarrow e & \mbox{from (10) and (3), with } p=(b \land d) \\ (12): & \lnot \textit{true} & \implies & \textit{false} & \mbox{from (11) and (4), with } p=(a \rightarrow e) \\ \end{array}</math> From a comparison of both deductions, the following issues can be seen: * Traugott's rule may yield a sharper resolvent: compare (5) and (10), which both resolve (1) and (2) on <math>p=c</math>. * Murray's rule introduced 3 new disjunction symbols: in (5), (6), and (7), while Traugott's rule did not introduce any new symbol; in this sense, Traugott's intermediate formulas resemble the user's style more closely than Murray's. * Due to the latter issue, Traugott's rule can take advantage of the implication in assumption (4), using as <math>p</math> the [[atomic formula|non-atomic formula]] <math>a \rightarrow e</math> in step (12). Using Murray's rules, the semantically equivalent formula <math>e \lor \lnot a \lor \lnot a</math> was obtained as (7), however, it could not be used as <math>p</math> 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 <math>p_1</math> and <math>p_2</math> of <math>F</math> and <math>G</math>, respectively. If <math>\phi</math> is the most general unifier of <math>p_1</math> and <math>p_2</math>, then the generalized resolvent is <math>F\phi[\textit{true}] \lor G\phi[\textit{false}]</math>. While the rule remains sound if a more special substitution <math>\phi</math> is used, no such rule applications are needed to achieve completeness.{{citation needed|date=February 2019}}
Traugott's rule is generalized to allow several pairwise distinct subformulas <math>p_1, \ldots, p_m</math> of <math>F</math> and <math>p_{m+1}, \ldots, p_n</math> of <math>G</math>, as long as <math>p_1, \ldots, p_n</math> have a common most general unifier, say <math>\phi</math>. The generalized resolvent is obtained after applying <math>\phi</math> 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;<ref name="Traugott.1986"/>{{rp|401}} it is not clear whether his rule would remain complete if restricted to <math>p_1 = \cdots = p_m</math> and <math>p_{m+1} = \cdots = p_n</math>.<ref>Here, "<math>=</math>" denotes [[Term (logic)#Structural equality|syntactical term equality modulo renaming]]</ref>
== 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.<ref name="Rubio">{{cite book|chapter=7. Paramodulation-Based Theorem Proving |first1=Robert|last1=Nieuwenhuis|first2=Alberto|last2=Rubio|chapter-url=http://www.cmi.ac.in/~madhavan/courses/theorem-proving-2014/reading/Nieuwenhuis-Rubio.pdf |editor1-first=Alan J.A. |editor1-last=Robinson |editor2-first=Andrei |editor2-last=Voronkov |title=Handbook of Automated Reasoning |publisher=Elsevier |date=2001 |isbn=978-0-08-053279-0 |pages=371–444 |url={{GBurl|HxaWA4lep_kC|pg=PR9}}}}</ref>
== Implementations ==
* [[CARINE]] * [[GKC Theorem Prover|GKC]] * [[Otter (theorem prover)|Otter]] * [[Prover9]] * [[SNARK (theorem prover)|SNARK]] * [[SPASS]] * [[Vampire (theorem prover)|Vampire]] * [https://logictools.org Logictools] online prover
== See also == * [[Condensed detachment]] — an earlier version of resolution * [[Inductive logic programming]] * [[Inverse resolution]] * [[Logic programming]] * [[Method of analytic tableaux]] * [[SLD resolution]]
== Notes == {{Reflist}}
== References ==
* {{cite journal |last=[[John Alan Robinson|Robinson]] |first=J. Alan |title=A Machine-Oriented Logic Based on the Resolution Principle |journal=[[Journal of the ACM]] |year=1965|volume=12|issue=1|pages=23–41 |doi=10.1145/321250.321253 |s2cid=14389185 |doi-access=free }} * {{cite book | last = Leitsch | first = Alexander |isbn=978-3-642-60605-2 |url={{GBurl|81LmCAAAQBAJ|p=1}} | title = The Resolution Calculus | publisher = [[Springer Science+Business Media|Springer]] | year = 1997 |series=Texts in Theoretical Computer Science. An EATCS Series }} * {{cite book | last = Gallier | first = Jean H. | authorlink = Jean Gallier | title = Logic for Computer Science: Foundations of Automatic Theorem Proving | publisher = [[Harper & Row]] | year = 1986 | url = http://www.cis.upenn.edu/~jean/gbooks/logic.html }} * {{cite book |last=Lee |first=Chin-Liang Chang, Richard Char-Tung |title=Symbolic logic and mechanical theorem proving |year=1987 |publisher=Academic Press |isbn=0-12-170350-9 |url-access=registration |url=https://archive.org/details/symboliclogicmec00chan }}
== External links == * {{MathWorld | urlname=ResolutionPrinciple | title=Resolution Principle | author=Alex Sakharov}} * {{MathWorld | urlname=Resolution | title=Resolution | author=Alex Sakharov}}
[[Category:1965 introductions]] [[Category:Automated theorem proving]] [[Category:Propositional calculus]] [[Category:Proof theory]] [[Category:Rules of inference]] [[Category:Theorems in propositional logic]]