Differences

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

--- sav08:classical_decision_problem [2008/04/02 17:18]
vkuncak
+++ sav08:classical_decision_problem [2008/04/02 23:06]
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 $\forall x_1. \ldots. \forall x_n. \exists y_1.\ldots \exists y_n. F$)
+  * 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 study is denoted
+===== References =====
   * [[http://www.logic.rwth-aachen.de/pub/graedel/Gr-kalmar03.ps|Decidable Classes of First-Order and Fixpoint Logics]]