Satisfiability of formulae with one \(\forall\) is decidable in exponential time
From MaRDI portal
Publication:915716
DOI10.1007/BF01651329zbMath0703.03002MaRDI QIDQ915716
Publication date: 1990
Published in: Archive for Mathematical Logic (Search for Journal in Brave)
satisfiability problems; first order logic without function symbols; full first order logic; maximal solvable classes; NEXPTIME-complete; quantifier prefix classes
03B10: Classical first-order logic
03B25: Decidability of theories and sets of sentences
03D15: Complexity of computation (including implicit computational complexity)
68Q15: Complexity classes (hierarchies, relations among complexity classes, etc.)
Related Items
On the Decision Problem for Two-Variable First-Order Logic, Testable and untestable classes of first-order formulae
Cites Work
- 0-1 laws and decision problems for fragments of second-order logic
- Complexity results for classes of quantificational formulas
- ENTSCHEIDUNGSPROBLEM REDUCED TO THE AEA CASE
- The unsolvability of the Gödel class with identity
- Alternation
- The decision problem for standard classes
- A note on the Entscheidungsproblem
- On Computable Numbers, with an Application to the Entscheidungsproblem
- Contributions to the reduction theory of the decision problem