On Stronger Calculi for QBFs

TL;DR

This paper explores advanced proof calculi for Quantified Boolean Formulas (QBFs), demonstrating how translations to first-order logic and novel instantiation rules can enhance deductive power and mimic complex quantifier manipulations.

Contribution

It introduces stronger QBF calculi by combining first-order resolution translations with variable instantiation and propositional extension rules, enabling more expressive proof systems.

Findings

First-order resolution can polynomially simulate QBF deduction concepts.

Enhanced calculus allows instantiation of universal variables by smaller existential variables.

Combining with propositional extension mimics general quantifier rules from sequent systems.

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.