Davis–Putnam algorithm: Difference between revisions

Revision as of 16:55, 5 April 2006

Revision as of 17:04, 26 June 2006

Line 12:

==References==

* M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. ''[[Communications of the ACM]]'', 5(7):394-397394–397, 1962.

* M. Davis and H. Putnam. A computing procedure for quantification theory. ''[[Journal of the ACM]]'', 7:201-215201–215, 1960.

* R. Dechter and I. Rish. Directional resolution: The Davis-Putnam procedure, revisited. In ''Proceedings of the Fourth International Conference on the Principles of Knowledge Representation and Reasoning (KR'94)'', pages 134-145134–145, 1994.

[[Category: Logical calculi]]

[[Category:Algorithms]]

[[de:Davis-Putnam-Verfahren]]