On Stronger Calculi for QBFs

DOI10.1007/978-3-319-40970-2_26zbMATH Open1475.68434arXiv1604.06483OpenAlexW2494237651MaRDI QIDQ2818031FDOQ2818031

Authors: Uwe Egly 

Publication date: 5 September 2016

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

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.

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

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

Mathematics Subject Classification ID

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

Cites Work

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

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
• Title not available (Why is that?)
• \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
• On QBF Proofs and Preprocessing
• On Stronger Calculi for QBFs
• Title not available (Why is that?)
• Strong (D)QBF dependency schemes via tautology-free resolution paths

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)