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/03 13:34]
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
+  * 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]]