Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
sav08:semidecision_procedure_for_first-order_logic_without_equality [2008/03/20 12:21] vkuncak created |
sav08:semidecision_procedure_for_first-order_logic_without_equality [2009/05/14 13:20] (current) vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Semidecision Procedure for Validity of Formulas in First-Order Logic ====== | ====== Semidecision Procedure for Validity of Formulas in First-Order Logic ====== | ||
+ | |||
+ | [[wp>Davis–Putnam algorithm]] (see [[http://www.cs.nyu.edu/cs/faculty/davism/|Martin Davis]], [[wp>Martin Davis]] and [[wp>Hilary Putnam]]) | ||
Suppose $S$ has no model. | Suppose $S$ has no model. | ||
Line 5: | Line 7: | ||
Then $propExpand(S)$ has no model. | Then $propExpand(S)$ has no model. | ||
- | By compactness, some finite subset has no model. | + | By propositional [[Compactness Theorem]], some finite subset has no model. |
Can check satisfiability of larger and larger initial prefixes of $propExpand(S)$ using a SAT solver. | Can check satisfiability of larger and larger initial prefixes of $propExpand(S)$ using a SAT solver. |