Revision as of 01:21, 23 May 2008 edit Rgrig (talk \| contribs) 72 edits mNo edit summary ← Previous edit		Revision as of 01:29, 23 May 2008 edit undo Rgrig (talk \| contribs) 72 edits mNo edit summary Next edit →
Line 4: The procedure roughly consists of these three parts: * ~~putting~~put the formula in [[prenex]] form and eliminate quantifiers * ~~generating~~generate one by one all ground instances * ~~checking~~...and ifcheck afor ~~ground~~each if ~~instance~~it is satisfiable The last part is probably the most innovative one, and works as follows:

Davis–Putnam algorithm: Difference between revisions