Talk:Resolution (logic)

From Wikipedia, the free encyclopedia

	Philosophy Portal This article is within the scope of the WikiProject Philosophy, which collaborates on articles related to philosophy. To participate, you can edit this article or visit the project page for more details.
???	This article has not yet received a rating on the quality scale.
Mid	This article has been rated as mid-importance on the importance scale.
Additional information: Related task forces (core areas): Logic

Contents 1 Math 2 GOFAI 3 Computability 4 Quick question 5 literals 6 uncomplete rule

[edit] Math

Shouldn't expressions like ∀X P(X) implies Q(X) be replaced by proper math environments? For one thing, all I see is a square infront 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.

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

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

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

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

[edit] uncomplete 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 disjonction, - 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 litteral) 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 litterals 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)