Differences
This shows you the differences between two versions of the page.
| Next revision Both sides next 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 12:49] vkuncak |
||
|---|---|---|---|
| Line 5: | Line 5: | ||
| 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. | ||