On Stronger Calculi for QBFs

DOI10.1007/978-3-319-40970-2_26MaRDI QIDQ2818031zbMATH OpenOpenAlexFDO

Authors Uwe Egly

Publication date 5 September 2016

Published in Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1604.06483

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Abstract: Quantified Boolean formulas (QBFs) generalize propositional formulas by admitting quantifications over propositional variables. QBFs can be viewed as (restricted) formulas of first-order predicate logic and easy translations of QBFs into first-order formulas exist. We analyze different translations and show that first-order resolution combined with such translations can polynomially simulate well-known deduction concepts for QBFs. Furthermore, we extend QBF calculi by the possibility to instantiate a universal variable by an existential variable of smaller level. Combining such an enhanced calculus with the propositional extension rule results in a calculus with a universal quantifier rule which essentially introduces propositional formulas for universal variables. In this way, one can mimic a very general quantifier rule known from sequent systems.

Recommendations

• On QBF Proofs and Preprocessing
• New resolution-based QBF calculi and their proof complexity
• On Unification of QBF Resolution-Based Calculi
• Proof complexity of resolution-based QBF calculi
• QBF as an alternative to Courcelle's theorem
• Theory and Applications of Satisfiability Testing
• Local soundness for QBF calculi
• Higher-order quantification and proof search
• scientific article; zbMATH DE number 4059375
• Logical Approaches to Computational Barriers

Cites work

• scientific article; zbMATH DE number 48763 (Why is no real title available?)
• scientific article; zbMATH DE number 819737 (Why is no real title available?)
• A solver for QBFs in negation normal form
• A structure-preserving clause form translation
• Contributions to the theory of practical quantified Boolean formula solving
• Normal form transformations
• On Stronger Calculi for QBFs
• On Unification of QBF Resolution-Based Calculi
• On sequent systems and resolution for QBFs
• Proof complexity of resolution-based QBF calculi
• QBF Resolution Systems and Their Proof Complexities
• Quantified propositional calculus and a second-order theory for NC\(^{\text \textbf{1}}\)
• Resolution for quantified Boolean formulas
• The intractability of resolution
• Unified QBF certification and its applications
• Variable dependencies and Q-resolution

Cited in

(14)

• Lower bound techniques for QBF expansion
• Efficient reduction of nondeterministic automata with application to language inclusion testing
• Lifting QBF resolution calculi to DQBF
• Building strategies into QBF proofs
• Local soundness for QBF calculi
• QBF as an alternative to Courcelle's theorem
• On sequent systems and resolution for QBFs
• Déjà Q All Over Again: Tighter and Broader Reductions of q-Type Assumptions
• scientific article; zbMATH DE number 7228403 (Why is no real title available?)
• \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
• On QBF Proofs and Preprocessing
• On Stronger Calculi for QBFs
• scientific article; zbMATH DE number 7029312 (Why is no real title available?)
• Strong (D)QBF dependency schemes via tautology-free resolution paths

Describes a project that uses

Uses Software

• Quaffle

This page was built for publication: On Stronger Calculi for QBFs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2818031)