Preprocessing in higher-order reasoning : learning from QBF solving

Abstract

In this thesis we present some preprocessing techniques for theorem proving in higher-order logic which are based on preprocessing techniques for quantified Boolean formulas. Higher-Order Logic (HOL) is a language which extends the well-known first-order logic with support for quantification over predicates and functions. In particular, we are interested in the development of automatic theorem provers for this logic. Automatic theorem provers attempt to find proofs for Hᴏᴌ formulas without further user input. One such system is Leo-III. Quantified Boolean Formulas (QBF), on the other hand, are an extension of propositional logic with explicit quantification over truth values. The validity of QBFs is, in contrast to HOL, decidable. Since HOL also supports quantification over truth values it is possible to translate every QBF into an equivalent HOL formula. We also discuss DQBF, an extension of QBF. Most modern QBF solving systems apply a preprocessing step before they start solving the input problem. Often this is done by invoking an external preprocessing tool. The output of the preprocessing tool is a potentially easier, but equivalent problem. We investigated whether it is possible to adapt some of the techniques used by QBF preprocessing systems to HOL. Towards this end, we give an overview of common QBF preprocessing techniques and present four algorithms for HOL. Universal reduction allows the removal of literals from clauses if they are universally quantified and appear in no other literal of the clause. Constant extraction uses a SAT solver to find literals necessary implied by the problem and adds them as a unit clause. Blocked clause elimination allows the removal of clauses if all resolvents on a literal are tautological. Our adaption uses pattern literals and works for problems without equality. Finally, first-order re-encoding wraps literals in a fresh proposition to delay primitive substitution. All four preprocessing techniques were implemented in the Leo-III theorem prover. To evaluate the performance of Leo-III and Leo-III augmented with our techniques on QBF and DQBF problems, we developed two flexible tools which translate those problems into HOL. Unfortunately, Leo-III could only solve a few of these. Hence, we evaluate the impact of our preprocessing techniques on HOL problems instead.