Complexity results for classes of quantificational formulas

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

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

Classical first-order logic (03B10) Complexity of computation (including implicit computational complexity) (03D15) Turing machines and related notions (03D10)

Related Items (48)

Universal quantifiers and time complexity of random access machines ⋮ The guarded fragment with transitive guards ⋮ A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ Problem solving by searching for models with a theorem prover ⋮ Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances ⋮ Second-Order Quantifier Elimination on Relational Monadic Formulas – A Basic Method and Some Less Expected Applications ⋮ Sufficient-completeness, ground-reducibility and their complexity ⋮ XML Schema Mappings ⋮ On the complexity of the two-variable guarded fragment with transitive guards ⋮ Using resolution for deciding solvable classes and building finite models ⋮ NEXP-Completeness and Universal Hardness Results for Justification Logic ⋮ The most nonelementary theory ⋮ Data Centric Workflows for Crowdsourcing ⋮ Two-Variable Separation Logic and Its Inner Circle ⋮ Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic ⋮ NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment ⋮ INTERLEAVING LOGIC AND COUNTING ⋮ Classifying the computational complexity of problems ⋮ On the Decision Problem for Two-Variable First-Order Logic ⋮ Testable and untestable classes of first-order formulae ⋮ Satisfiability of formulae with one \(\forall\) is decidable in exponential time ⋮ The complexity of Bayesian networks specified by propositional and relational languages ⋮ Efficiently solving quantified bit-vector formulas ⋮ Symbolic backward reachability with effectively propositional logic. Application to security policy analysis ⋮ On logics with two variables ⋮ 0-1 laws and decision problems for fragments of second-order logic ⋮ Deciding Effectively Propositional Logic Using DPLL and Substitution Sets ⋮ Average case completeness ⋮ Complexity of fixed-size bit-vector logics ⋮ Complexity Assessments for Decidable Fragments of Set Theory. I: A Taxonomy for the Boolean Case* ⋮ Random models and the Gödel case of the decision problem ⋮ What’s Decidable About Program Verification Modulo Axioms? ⋮ Deciding effectively propositional logic using DPLL and substitution sets ⋮ First-order logic with two variables and unary temporal logic ⋮ First-order definable counting-only queries ⋮ Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates ⋮ SAT vs. Translation Based decision procedures for modal logics: a comparative evaluation ⋮ Lifting QBF Resolution Calculi to DQBF ⋮ SCL clause learning from simple models ⋮ Set constraints in some equational theories ⋮ Set constraints in some equational theories ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ Relational transducers for electronic commerce ⋮ Tarskian set constraints ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ The complexity of the satisfiability problem for Krom formulas ⋮ On computational complexity of Prolog programs ⋮ Complete problems in the first-order predicate calculus

Cites Work

This page was built for publication: Complexity results for classes of quantificational formulas