Talk:Resolution (logic)

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Philosophy (Rated Start-class, Mid-importance)
WikiProject icon This article is within the scope of WikiProject Philosophy, a collaborative effort to improve the coverage of content related to philosophy on Wikipedia. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the general discussion about philosophy content on Wikipedia.
Start-Class article Start  This article has been rated as Start-Class on the project's quality scale.
 Mid  This article has been rated as Mid-importance on the project's importance scale.
 

Math[edit]

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[edit]

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[edit]

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[edit]

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 (talkcontribs) 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[edit]

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[edit]

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[edit]

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[edit]

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[edit]

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)