Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
|
sav08:semidecision_procedure_for_first-order_logic_without_equality [2009/05/14 13:19] vkuncak |
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]] | + | [[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. | ||