Revision as of 21:28, 21 May 2015 edit Jochen Burghardt (talk \| contribs) Extended confirmed users 24,310 edits →Technical ← Previous edit		Revision as of 21:30, 21 May 2015 edit undo Jochen Burghardt (talk \| contribs) Extended confirmed users 24,310 edits →Sloppy algorithm description Next edit →
Line 28: :∀''x''. ∃''y''. ''y''>''x'' ∧ ''p''(''y''), we get after quantifier elimination (i.e. [[Skolemization]], with ''f'' being a Skolem function for ''y''): :''f''(''x'')>''x'' ∧ ''p''(''f''(''x'')''),

Talk:Davis–Putnam algorithm: Difference between revisions