Chapter 29. Theory of Quantified Boolean Formulas

Quantified Boolean formulas (QBF) are a generalization of propositional formulas by allowing universal and existential quantifiers over variables. This enhancement makes QBF a concise and natural modeling language in which problems from many areas, such as planning, scheduling or verification, can often be encoded in a more compact way than with propositional formulas. We introduce in this chapter the syntax and semantics of QBF and present fundamental concepts. This includes normal form transformations and Q-resolution, an extension of the propositional resolution calculus. In addition, Boolean function models are introduced to describe the valuation of formulas and the behavior of the quantifiers. We also discuss the expressive power of QBF and provide an overview of important complexity results. These illustrate that the greater capabilities of QBF lead to more complex problems, which makes it interesting to consider suitable subclasses of QBF. In particular, we give a detailed look at quantified Horn formulas (QHORN) and quantified 2-CNF (Q2-CNF).

Efficient Local Reductions to Basic Modal Logic

We present novel reductions of the propositional modal logics "Image missing" , "Image missing" , "Image missing" , "Image missing" and "Image missing" to Separated Normal Form with Sets of Modal Levels. The reductions result in smaller formulae than the well-known reductions by Kracht and allow us to use the local reasoning of the prover "Image missing" to determine the satisfiability of modal formulae in these logics. We show experimentally that the combination of our reductions with the prover "Image missing" performs well when compared with a specialised resolution calculus for these logics and with the b̆uilt-in reductions of the first-order prover SPASS.

Schematic Refutations of Formula Schemata

Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.

A resolution calculus for MinSAT

The logical calculus for SAT are not valid for MaxSAT and MinSAT because they preserve satisfiability but not the number of unsatisfied clauses. To overcome this drawback, a MaxSAT resolution rule preserving the number of unsatisfied clauses was defined in the literature. This rule is complete for MaxSAT when it is applied following a certain strategy. In this paper we first prove that the MaxSAT resolution rule also provides a complete calculus for MinSAT if it is applied following the strategy proposed here. We then describe an exact variable elimination algorithm for MinSAT based on that rule. Finally, we show how the results for Boolean MinSAT can be extended to solve the MinSAT problem of the multiple-valued clausal forms known as signed conjunctive normal form formulas.

Complexity of translations from resolution to sequent calculus

Resolution and sequent calculus are two well-known formal proof systems. Their differences make them suitable for distinct tasks. Resolution and its variants are very efficient for automated reasoning and are in fact the theoretical basis of many theorem provers. However, being intentionally machine oriented, the resolution calculus is not as natural for human beings and the input problem needs to be pre-processed to clause normal form. Sequent calculus, on the other hand, is a modular formalism that is useful for analysing meta-properties of various logics and is, therefore, popular among proof theorists. The input problem does not need to be pre-processed, and proofs are more detailed. However, proofs also tend to be larger and more verbose. When the worlds of proof theory and automated theorem proving meet, translations between resolution and sequent calculus are often necessary. In this paper, we compare three translation methods and analyse their complexity.

BDI: A New Decidable First-order Clause Class

BDI (Bounded Depth Increase) is a new decidablefirst-order clause class. It strictly includesknown classes such as PVD. The arityof function and predicate symbols as well as theshape of atoms is not restricted in BDI. Insteadthe shape of "cycles" in resolution inferences isrestricted such that the depth of generated clausesmay increase but is still finitely bound.The BDI class is motivated by real world problemswhere function terms are used to represent record structures.We show that the hyper-resolution calculus moduloredundancy elimination terminates on BDI clause sets.Employing this result to the ordered resolution calculus,we can also prove termination of ordered resolution on BDI,yielding a more efficient decision procedure.

A Resolution Calculus for Second-order Logic with Eager Unification

The efficiency of the first-order resolution calculus is impaired when lifting it to higher-order logic. The main reason for that is the semi-decidability and infinitary natureof higher-order unification algorithms, which requires the integration of unification within the calculus and results in a non-efficient search for refutations.We present a modification of the constrained resolution calculus (Huet'72) which uses an eager unification algorithm while retaining completeness. Thealgorithm is complete with regard to bounded unification only, which for many cases, does not pose a problem in practice.