Talk:Resolution (logic)

From Wikipedia, the free encyclopedia

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