Davis–Putnam algorithm: Difference between revisions

Revision as of 21:42, 24 September 2005

Revision as of 19:40, 27 September 2005

Line 15:

* [[Martin Davis]]

* [[Hilary Putnam]]

==References==

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

* M. Davis and H. Putnam. A computing procedure for quantification theory. ''Journal of the ACM'', 7:201-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-145, 1994.

{{Mathlogic-stub}}