Differences

This shows you the differences between two versions of the page.

--- sav08:classical_decision_problem [2008/04/02 17:14]
vkuncak created
+++ sav08:classical_decision_problem [2008/04/02 23:57]
vkuncak
@@ Line 1: / Line 1: @@
 ====== Classical Decision Problem ======
+Consider satisfiability problem for sentences in first-order logic.
+Without loss of generality, assume that formulas are in prenex form.
+Classify formulas according to
+  * presence or absence of equality in formulas
+  * regular expression describing the sequence of quantifiers (e.g. $\exists^* \forall^*$ means formulas $\exists x_1. \ldots. \exists x_n. \forall y_1.\ldots \forall y_m. F$ where $F$ is quantifier-free)
+  * number and arity of relation symbols
+  * number and arity of function symbols
+For each such description, determine whether the subsets of formulas that satisfy it are decidable or not.
+Example: the exists-forall class that we will look at shortly is denoted $[\exists^* \forall^*,all,(0)]_{=}$.
+===== References =====
   * [[http://www.logic.rwth-aachen.de/pub/graedel/Gr-kalmar03.ps|Decidable Classes of First-Order and Fixpoint Logics]]
+  * [[http://www.di.unipi.it/~boerger/decpblbook.html|Egon Börger, Erich Grädel, Yuri Gurevich: The Classical Decision Problem]], also on [[http://books.google.ch/books?id=3po2Tv_UVcMC&vq=On+the+classical+decision+problem|Google Books]]