Davis-Putnam algorithm

From Wiktionary, the free dictionary
Jump to navigation Jump to search

English[edit]

Etymology[edit]

Developed by Martin Davis and Hilary Putnam.

Proper noun[edit]

the Davis-Putnam algorithm

  1. (logic) An algorithm for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic.

Related terms[edit]