|In 1960, Davis-Putnam
procedure was introduced as a theorem-proving technique suitable for
automation. It deals with classical propositional and first-order logic.
|Davis-Putnam procedure deals
with a disjunction of clause sets, called a block.
|This procedure involves
repeated rewriting of a block into an equivalent block using simple rewriting
rules. Each of these rewriting rules takes some clause set in a block and
replace it by one or more of others. The aim is to produce a block that can
easily be seen as satisfactory or not.