Satisfiability of formulae with one \(\forall\) is decidable in exponential time

DOI10.1007/BF01651329zbMath0703.03002OpenAlexW110461417MaRDI QIDQ915716

Erich Grädel

Publication date: 1990

Published in: Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf01651329

zbMATH Keywords

satisfiability problemsfirst order logic without function symbolsfull first order logicmaximal solvable classesNEXPTIME-completequantifier prefix classes

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Complexity of computation (including implicit computational complexity) (03D15) Complexity classes (hierarchies, relations among complexity classes, etc.) (68Q15)

Related Items (2)

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

This page was built for publication: Satisfiability of formulae with one \(\forall\) is decidable in exponential time