Bibliographic Metadata

Preprocessing in higher-order reasoning : learning from QBF solving / von Hans Jörg Schurr
Additional Titles
Preprocessing Techniken für schnellere Inferenz mit boolschen Typen im automatischen Beweisen in der Logik höherer Stufe
AuthorSchurr, Hans Jörg
CensorLeitsch, Alexander
PublishedWien, 2017
Description102 Seiten : Diagramme
Institutional NoteTechnische Universität Wien, Diplomarbeit, 2017
Zusammenfassung in deutscher Sprache
Abweichender Titel nach Übersetzung der Verfasserin/des Verfassers
Document typeThesis (Diplom)
Keywords (DE)automatische Deduktion / Quantifizierte boolsche Logik
Keywords (EN)automated deduction / quantified Boolean logic
URNurn:nbn:at:at-ubtuw:1-103744 Persistent Identifier (URN)
 The work is publicly available
Preprocessing in higher-order reasoning [0.6 mb]
Abstract (English)

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.

The PDF-Document has been downloaded 20 times.