Revision as of 00:50, 30 August 2008 edit Linas (talk \| contribs) 25,539 edits Herbrandization ← Previous edit		Revision as of 01:04, 30 August 2008 edit undo Linas (talk \| contribs) 25,539 edits err, undo what I did Next edit →
Line 4: The procedure roughly consists of these three parts: * put the formula in [[prenex]] form and eliminate quantifiers ~~([[Herbrandization]])~~ * generate one by one all ground instances * ...and check for each if it is satisfiable Line 22: [[DPLL algorithm]] [[Herbrandization]] ==References==

Davis–Putnam algorithm: Difference between revisions