Talk:Davis–Putnam algorithm

This article is rated Stub-class on Wikipedia's content assessment scale.
It is of interest to the following WikiProjects:

Computing

	This article is within the scope of WikiProject Computing, a collaborative effort to improve the coverage of computers, computing, and information technology on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.ComputingWikipedia:WikiProject ComputingTemplate:WikiProject ComputingComputing articles
???	This article has not yet received a rating on the project's importance scale.
	This article has been automatically rated by a bot or other tool because one or more other projects use this class. Please ensure the assessment is correct before removing the `\|auto=` parameter.

Mathematics Low‑priority

	Mathematics portal This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.MathematicsWikipedia:WikiProject MathematicsTemplate:WikiProject Mathematicsmathematics articles
Low	This article has been rated as Low-priority on the project's priority scale.

Move?

User:Jon Awbrey (now permanently blocked) moved this article from Davis-Putnam algorithm to Davis-Putnam algorithm (if that's too subtle to see, he replaced the simple hyphen with a slightly longer en dash. While some manuals of style recommend this, I don't think it is appropriate here - Wikipedia rule is to use the most well-known name, and most people do not even know about different dashes, let alone how to type them on a normal keyboard (the last includes me...). So I suggest to move it back. Any coments? --Stephan Schulz 06:48, 7 September 2006 (UTC)[reply]

The long dash convention was a math project one. In my opinion, it was a bad choice; anyway, this article is about computer science, so I do not see how that convention affects this article User:Tizio. 11:09, 15 September 2006 (UTC)[reply]

As of the now, the manual of style recommends the en dash, so I've moved it back. Algebraist 12:32, 26 May 2008 (UTC)[reply]

Jon may have committed crimes, but en-dash wasn't one of them. linas (talk) 00:53, 30 August 2008 (UTC)[reply]

Technical

What is a ground formula? Also, I can read the Resolution (logic) article without problem, and while I'm not a logic expert, I studied a bit about first order logic and resolution in some courses, so definitely the article is not accessible enough currently, IMHO. --Blaisorblade (talk) 19:03, 8 October 2008 (UTC)[reply]

the problem is not being too technical. It's about missing the definition of "ground instance". The article is written accessibly enough that I get the feeling if it were defined, things would be a lot clearer. I'll add the appropriate tag and remove the inappropriate technical tag. --C S (talk) 12:12, 25 October 2008 (UTC)[reply]

Sloppy algorithm description

Meanwhile, ground instance has a redirect link. However, ground instance don't have any variables, so the "last part" doesn't make sense in the current form. I don't have access to the original article, but I guess "generate all propositional ground instances" is a sloppy phrase for "generate all ground instances; for each of them, replace each ground atom by a unique propositional variable".

As an example, starting from

∀x. ∃y. y>x ∧ p(y),

we get after quantifier elimination (i.e. Skolemization, with f being a Skolem function for y):

f(x)>x ∧ p(f(x)),

which has the ground instances (assuming, e.g., natural numbers' constructors - I'm not sure about this point):

f(0)>0 ∧ p(f(0)),

f(s(0))>s(0) ∧ p(f(s(0))),

f(s(s(0)))>s(s(0)) ∧ p(f(s(s(0)))),

f(s(s(s(0))))>s(s(s(0))) ∧ p(f(s(s(s(0))))),

...

(that is the meaning of "one by one": there may be infinitely many ground instances, all of which have to be checked in succession until an unsatisfiable one is found). To check e.g. the first one, convert it into a propositional formula by introducing A for f(0)>0, and B for p(f(0)), leading to

A ∧ B

which is then shown to be satisfiable by the "last part" (there is nothing to resolve here; however de:Davis-Putnam-Verfahren#Regeln lists several other rules, the One-Literal rule would be applicable). In this, admittedly poor, example, all ground instances lead to the propositional formula A∧B. - Jochen Burghardt (talk) 21:28, 21 May 2015 (UTC)[reply]