Revision as of 20:39, 29 June 2008 edit Alaibot (talk \| contribs) 434,501 edits m Robot: sorting stub (based on existing categorisation) ← Previous edit		Revision as of 00:50, 30 August 2008 edit undo Linas (talk \| contribs) 25,539 edits Herbrandization 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

Davis–Putnam algorithm: Difference between revisions