Complexity results for classes of quantificational formulas

DOI10.1016/0022-0000(80)90027-6zbMath0471.03034WikidataQ59650026 ScholiaQ59650026MaRDI QIDQ1157324

Harry R. Lewis

Publication date: 1980

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(80)90027-6

Mathematics Subject Classification ID

03B10: Classical first-order logic

03D15: Complexity of computation (including implicit computational complexity)

03D10: Turing machines and related notions

Related Items

On the Decision Problem for Two-Variable First-Order Logic, SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation, Testable and untestable classes of first-order formulae, The most nonelementary theory, The complexity of the satisfiability problem for Krom formulas, On the complexity of the two-variable guarded fragment with transitive guards, Satisfiability of formulae with one \(\forall\) is decidable in exponential time, 0-1 laws and decision problems for fragments of second-order logic, Deciding effectively propositional logic using DPLL and substitution sets, Complete problems in the first-order predicate calculus, Average case completeness, Set constraints in some equational theories, On computational complexity of Prolog programs, Problem solving by searching for models with a theorem prover, Relational transducers for electronic commerce, Tarskian set constraints, The guarded fragment with transitive guards, On logics with two variables, Efficiently solving quantified bit-vector formulas, Symbolic backward reachability with effectively propositional logic. Application to security policy analysis, First-order logic with two variables and unary temporal logic, Sufficient-completeness, ground-reducibility and their complexity, XML Schema Mappings, NEXP-Completeness and Universal Hardness Results for Justification Logic, Random models and the Gödel case of the decision problem, Deciding Effectively Propositional Logic Using DPLL and Substitution Sets, Universal quantifiers and time complexity of random access machines, Classifying the computational complexity of problems

Cites Work

• Complete problems in the first-order predicate calculus
• A \(2^{2^{2^{pn}}}\) upper bound on the complexity of Presburger arithmetic
• A hierarchy for nondeterministic time complexity
• Solvable cases of the decision problem
• Classification of $AEA$ formulas by letter atoms
• Satisfiability problems for propositional calculi
• Linear sampling and the ∀∃∀ case of the decision problem
• Description of restricted automata by first-order formulae
• Turing machines and the spectra of first-order formulas
• On the Computational Complexity of Algorithms
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item