LARA

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