Differences

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

--- sav08:classical_decision_problem [2008/04/02 23:03]
vkuncak
+++ sav08:classical_decision_problem [2008/04/03 13:34]
vkuncak
@@ Line 6: / Line 6: @@
 Classify formulas according to
-  * regular expression describing the sequence of quantifiers (e.g. $\exists^* \forall^*$ means formulas $\forall x_1. \ldots. \forall x_n. \exists y_1.\ldots \exists y_n. F$)
+  * 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)
+  * sequence of numbers of relation symbols for each arity
+  * sequence of numbers of function symbols for each arity
+  * presence or absence of equality in formulas
+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]]