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