Talk:Resolution (logic)

Merger proposal

I believe Resolution inference should in fact be merged into the current page, carrying over the references from there as additional references. — Preceding unsigned comment added by Vkuncak (talk • contribs) 13:13, 23 June 2021 (UTC)

Math

Shouldn't expressions like he was an man who ∀X P(X) implies Q(X) be replaced by proper math environments? For one thing, all I see is a square in front of that X, but secondly, it just looks better and is more readily absorbed by the reader. I've started converting the page, but lower down I didn't understand the maths (due to the little squares where there should be symbols), so someone else can do the rest.

GOFAI

On 22 September 2005, [Paolo Liberatore] edited this page deleting a sentence at the beginning of the article. That sentence claimed that automated theorem proving is a branch of AI. In the literature I have read, for example "Artificial Intelligence, a Modern Approach" (probably the most complete book about GOFAI), automated theorem proving is considered a subject of GOFAI. I agree with that and thus I think it should be included in the article changing "branch" for "subject", because there are other disciplines dealing with automated theorem proving. [Ivan F. Villanueva B.]

I don't mind either way. Maybe AI should be mentioned in automated theorem proving instead? If you have a strong opinion, be bold. BTW, I don't think the term GOFAI should be overused - it's a nice gag, but it should be enough to have a small paragraph linked from the main AI page. --Stephan Schulz 09:50, 23 September 2005 (UTC)

The current version of the first sentence is ok to me (subject is correct, branch was not), also because GOFAI is now an article and not a redirect. Paolo Liberatore (Talk) 11:16, 23 September 2005 (UTC)

Well, I have a strong opinion: The GOFAI link was distracting and self-indulgent, and the gag isn't actually particularly funny. Very bad style. Taking Stephan at his word, I deleted it. Jorend 13:03, 31 March 2006 (UTC)

Computability

I just started a computability section but I'm unsure of the facts -- my best try is there but tagged with question marks, could someone more expert than me check this and correct them please?

Sorry, I've deleted your section again. Computability is a property of the problem, not of the method used. Resolution can be used to implement a complete refutation procedure for first-order clause sets, and a complete decision procedure for finite propositional logic clause sets. But you need extra conditions (fairness) and operations. --Stephan Schulz 13:01, 1 December 2006 (UTC)

Quick question

What are complementary literals? They seem to be a literal and its negation. If someone knows that this is correct, could you just parenthetically say that in the article? It's unnecessarily opaque right now. —The preceding unsigned comment was added by SpaceMoose (talk • contribs) 03:48, 3 March 2007 (UTC).

I've tried, is it clearer now? The problem ist that one really needs to assume knowledge about clauses, literals, and atoms to write a decent description of resolution.--Stephan Schulz 10:16, 3 March 2007 (UTC)

Literals

Does resolution actually have to be done on a disjunction of literals? What if a clause has conjunctions? Fresheneesz (talk) 07:50, 18 November 2007 (UTC)

Resolution many other methods and systems require a normal form, here it is a "Conjunctive Normal Form" (CNF) and this is sufficient because every first order logic formula can be translated into a semantically equivalent formula in CNF. With my understanding (and the wiki page) the term "clause" refers only to a _disjunction_ or literals, thus by definition, a clause cannot have a conjunction. What you probably mean is that you have a general formula with a mixture of conjunctions and disjunctions and would like to apply this method. What you would do is you would convert your formula into CNF. This results in n clauses where you can perform pairwise resolution. See Conjunctive_normal_form#Conversion_into_CNF Methossant (talk) 22:35, 22 February 2009 (UTC)

Incomplete rule

The presented rule of resolution is the binary resolution. It is incomplete : the set of clauses, a+b, a+-b, -a+b, -a+-b is inconsistent (+ is the disjunction, - is the negation) but with this single rule, you obtain only resolvant of length 2. In order to have a complete system, you need either to add the factoring rule, from A+p+B+p+C (where p is a literal) deduce A+B+C either to define a more complex resolution rule, combining binary resolution and factorization either (following the Robinson founder of the resolution system) considering that a clause is a set of literals Liviusbarbatus (talk) 14:12, 30 January 2008 (UTC)

Notice that the end of the article acknowledges this point implicitly: "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." However, I agree with Liviusbarbatus: The point should be made more explicitly. Moreover, the point that clauses can be represented as sets of literals might be given more emphasis. In particular, the set theoretic definition of resolution is much simpler than the one given in this article. In the propositional case, the two clauses C - {L} and C' - {-L} have the resolvent C union C'. (I don't know how to insert set union.) Logperson (talk) 09:15, 31 January 2008 (UTC)

The orginal resolution rule by Robinson is a "full resolution", which works on resolving more than two literals at a time. Binary resolution together with factoring can be proven to be equivalent to the original full resolution (in the sense that both can deduce the same clauses). This remark could be added in the end (clarifying the confusion between "full" resolution and binary resolution + factoring), but preferably, the section would introduce full resolution and then binary resolution + factoring (if we want chronological order, for comprehension, it may be better to do the opposite). —Preceding unsigned comment added by 58.153.59.218 (talk) 13:29, 25 March 2010 (UTC)

Axioms / knowledge base

The article says if the empty clause can be derived, "the initial conjecture follows from the axioms". Are these axioms the knowledge base mentioned earlier (+ axioms of boolean algebra)? 84.238.30.199 (talk) 16:27, 12 October 2008 (UTC)

Contradiction

In the first paragraphs there seems to be a contradiction between the following two sentences. I suggest to rephrase the first one s.t. it does not say "all literals that have complements". PeterSchueller (talk) 08:15, 10 July 2009 (UTC)

"The resulting clause contains all the literals that do not have complements."
"However, only the pair of literals that are resolved upon can be removed: all other pair of literals remain in the
resolvent clause."

Confusing date

Isn't it confusing to assert that resolution is due to John Alan Robinson in 1965, in the first paragraph, and that it's used in DP-algorithm which publication date is more 1960 or 1962 for its revised version, at the end of the "Resolution in propositional logic" section ? It may be just that Davis and Putnam didn't call it that way, or that Robinson extended the idea, or that I'm just confused. The dates are from the bibliography from the resolution and the dpll articles. 131.254.10.81 (talk) 15:50, 27 July 2009 (UTC)

I agree. The resolution rule was not introduced by Robinson, but by Davis and Putnam in their original DP algorithm. Robinsons contribution is the use of unification, which avoids an exhaustive search for an empty clause through the set of all ground instances (see Herbrand's theorem for details on this). Resolution with unification instead resolves only those literals which can be unified, e.g. P(f(x)) is resolved with -P(f(c)) with substitution x := c. Robinson proved the important properties that if two atomic formulas are unifiable, there is a most general unifier (MGU), and there is (a straightforward) algorithm to compute a MGU (furthermore, MGUs are equivalent up to renaming). He then proved the Lifting Lemma, which essentially proves that Resolution+Unification is refutation-complete (intuitively, he showed that resolution+unification, which resolves far less clauses than exhaustive searches, does not lose refutation-completeness. Thus it is in generally preferable to use Robinsons resolution+unification instead of DP/DPLL for first-order theorem proving). I suggest these insights should be incorporated into the article. —Preceding unsigned comment added by 58.153.59.218 (talk) 18:01, 29 March 2010 (UTC)

I agree, and tried to rephrase the lead accordingly. Explanation of the role of MGU and Lifting Lemma in the article (maybe with an example contrasting DPLL and Robinson) still remains to be done. - Jochen Burghardt (talk) 23:48, 29 May 2014 (UTC)

Completeness proof sketch: text deleted from article

I undid the 10 edits of 19 Aug by 162.245.243.38. They mainly added a subsection "Completeness proof sketch" which I saved below. While I appreciate the addition of a completeness proof sketch, I have the following problems with the version of 162.245.243.38:

• The second lemma contains technical errors: the cartesian product is a set of tuples, not of sets; the latter would be required for clauses. The given example doesn't use the set notation at all.
• The theorem appears to require the given formula (or formula set) in DNF. It is not clear how to obtain from the theorem a resolution tree for an arbitrary formula, without converting it into DNF first.
• Its is not clear how to compose inductively found resolution subtrees.
• In step 2, I guess the chosen literal a needs to be replaced by TRUE and FALSE in the first and second cartesian product, respectively. I can't check my hunch since the proof doesn't say what to do with these products.
• At first glance, I couldn't find a proof in a text books that resembles the one given here.

Some, or all, issues may of course be fixable. - Jochen Burghardt (talk) 17:05, 21 August 2019 (UTC)

START OF SAVED TEXT

---

Completeness proof sketch

The existence of a resolution tree is equivalent to unsatisfiability. The foreward implication of this statement follows from inference properties discussed above (soundness). The backward implication (completeness) will be shown presently.

We will prove completeness of propositional resolution by examining the interplay of a formula's conjunctive normal form and disjunctive normal form.

Lemma: Unsatisfiability is equivalent to the existence of a pair of complementary literals ($a$ and $\neg a$) in every disjunctive normal form clause.

Proof: As DNF clauses are disjoined, the problem is unsatisfiable if and only if every clause is unsatisfiable. If a clause does not have a pair of complementary literals, one may generate a satisfying assignment by assigning TRUE to every positively-occuring literal and FALSE to every negatively-occuring literal.

Lemma: Suppose $C$ is a set of CNF clauses and the clauses are denoted as sets. Then $C_{1}\times C_{2}\times \ldots \times C_{n}$ is an equivalent set of DNF clauses. Likewise, suppose $D$ is a set of DNF clauses. Then $D_{1}\times D_{2}\times \ldots \times D_{m}$ is an equivalent set of CNF clauses.

Example: ${\Big (}(A\vee B)\land (C\vee D){\Big )}\Leftrightarrow {\Big (}(A\land C)\vee (A\land D)\vee (B\land C)\vee (B\land D){\Big )}$

Proof: Write $C=(C_{1,1}\lor C_{1,2}\lor \ldots )\land (C_{2,1}\lor C_{2,2}\lor \ldots )\land \ldots$. The lemma follows by repeated application of the principle of distributivity. The other case follows by symmetry of the distributive law in boolean algebra.

Theorem: Unsatisfiability implies the existence of a resolution tree.

Proof: By the first lemma, we have a set of DNF clauses, $D$, where each clause has a pair of complementary literals, $a$ and $\neg a$.

1. Choose the first clause $D_{1}$.
2. Consider all CNF clauses of the form $\{a\}\times D_{2}\times \ldots \times D_{n}$ and $\{\neg a\}\times D_{2}\times \ldots \times D_{n}$.
3. Resolve matching clauses together to get derivations for $D_{2}\times \ldots \times D_{n}$.
4. Proceed inductively until the empty disjunction is derived.

Example: Find a resolution tree for this unsatisfiable formula: $\neg ((A\vee B)\rightarrow (A\vee B))$.

Rewrite in disjunctive normal form as $(\neg A\land \neg B\land A)\vee (\neg A\land \neg B\land B)$.

1. Choose the first clause, $\neg A\land \neg B\land A$.
2. Consider the set of CNF clauses: ${\Big [}(A\vee \neg A)\land (A\vee \neg B)\land (A\vee B){\Big ]}\land {\Big [}(\neg A\vee \neg A)\land (\neg A\vee \neg B)\land (\neg A\vee B){\Big ]}$.
3. Resolve the n-th clause in the left bracket with the n-th clause in the right bracket to get three CNF clauses: $\neg A\land \neg B\land B$.
4. (1) Choose the remaining clause, $\neg A\land \neg B\land B$.
5. (2) Consider the set of CNF clauses: $B\land \neg B$.
6. (3) Resolve to get $\bot$.

The above procedure will have generated the following resolution tree:

${\dfrac {{\dfrac {A\vee B,\quad \neg A\vee B}{B}},\quad {\dfrac {A\vee \neg B,\quad \neg A\vee \neg B}{\neg B}}}{\bot }}$

---

END OF SAVED TEXT

Exhaustively applying resolution rule leading to a tautology

As this is my first participation on Wikipedia, I apologize if I am going against custom in one way or the other. In section "Resolution in propositional logic" the following is claimed

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

I cannot see how the last claim about always arriving at a tautology should be true. There are two cases, both of which are not going to be trivially true

1. We arrive at a non-empty clause. It is satisfiable, since it can be made true by setting any of the literals to be true. On the other hand, since it is non-empty and there are no complements, then the entire clause can evaluate to false by setting all literals to false.
2. We arrive at the empty clause, which is trivially false.

I assume, that there is some detail I've missed. Maybe it has to do with the goal of the resolution technique, described later in the article? Could this be elaborated?

--Soelvsten (talk) 07:25, 5 October 2020 (UTC)

If there are two pairs of complementary literals (e.g. $c,\lnot c$ and $\lnot d,d$), then the application of the resolution rule yields:

${\frac {\lnot d\lor a_{1}\lor a_{2}\lor \cdots \lor c,\quad d\lor b_{1}\lor b_{2}\lor \cdots \lor \neg c}{\lnot d\lor a_{1}\lor a_{2}\lor \cdots \lor d\lor b_{1}\lor b_{2}\lor \cdots }}$

That is, the resolvent on the first pair ($c,\lnot c$), containing the disjunction on the second pair ($\lnot d,d$), is satistifed by every assignment of truth values, hence a tautology. I guess most theorem provers would simplify it to ${\text{true}}$, and then discard it. Resolving the clauses on $\lnot d,d$ will obtain a similar result. - Jochen Burghardt (talk) 11:59, 5 October 2020 (UTC)