Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

The HolQbf Library

HolQbfLib provides a rudimentary platform for experimenting with combinations of theorem proving and Quantified Boolean Formulae (QBF) solvers. HolQbfLib was developed as part of a research project on Expressive Multi-theory Reasoning for Interactive Verification (EPSRC grant EP/F067909/1) from 2008 to 2011. It is loosely inspired by HolSatLib (Section 8.11), and has been described in parts in the following publications:

  • Tjark Weber: Validating QBF Invalidity in HOL4. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11–14, 2010. Proceedings, volume 6172 of Lecture Notes in Computer Science, pages 466–480. Springer, 2010.
  • Ramana Kumar and Tjark Weber: Validating QBF Validity in HOL4. In Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk, editors, Interactive Theorem Proving, Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22–25, 2011. Proceedings, volume 6898 of Lecture Notes in Computer Science, pages 168–183. Springer, 2011.

HolQbfLib uses an external QBF solver, Squolem, to decide Quantified Boolean Formulae.

Installing Squolem

HolQbfLib has been tested with (the x86 Linux version of) Squolem 2.02 (release date 2010-11-10). This is Squolem's latest version at the time of writing. Squolem can be obtained from http://www.cprover.org/qbv/download.html. After installation, you must make the executable available as squolem2, e.g., by placing it into a folder that is in your $PATH. This name is currently hard-coded: there is no configuration option to tell HOL about the location and name of the Squolem executable.

Interface

The library provides four functions, each of type term -> thm, to invoke Squolem: decide, decide_prenex, disprove, and prove. These are defined in the HolQbfLib structure, which is the library's main entry point.

Calling prove $\phi$ will invoke Squolem on the QBF $\phi$ to establish its validity. If this succeeds, prove will then validate the certificate of validity generated by Squolem in HOL to return a theorem $\vdash \phi$.

Similarly, calling disprove $\phi$ will invoke Squolem to establish that $\phi$ is invalid. If this succeeds, disprove will then validate the certificate of invalidity generated by Squolem in HOL to return a theorem $\phi \vdash \bot$.

decide_prenex $\phi$ combines the functionality of prove and disprove into a single function. It will invoke Squolem on $\phi$ and return either $\vdash \phi$ or $\phi \vdash \bot$, depending on Squolem's answer.

Finally, decide does the same job as decide_prenex but accepts QBFs in a less restricted form. Restrictions on $\phi$ are described below.

Figure: HolQbfLib in action.

- load "HolQbfLib";
metis: r[+0+3]#
r[+0+6]#
> val it = () : unit

- open HolQbfLib;
> val decide = fn: term -> thm
val decide_prenex = fn: term -> thm
val disprove = fn: term -> thm
val prove = fn: term -> thm

- show_assums := true;
> val it = () : unit

- decide ``?x. x``;
<<HOL message: HolQbfLib: calling external command
  'squolem2 -c /tmp/filedH1K2x >/dev/null 2>&1'>>
> val it =  [] |- ?x. x: thm

- decide ``(?y. x \/ y) ==> ~x``;
> val it = [!x. (?y. x \/ y) ==> ~x] |- F: thm

- decide ``~(?x. x ==> y) \/ (?x. y ==> x)``;
<<HOL message: HolQbfLib: calling external command
  'squolem2 -c /tmp/fileyap3oD >/dev/null 2>&1'>>
> val it = [] |- ~(?x. x ==> y) \/ ?x. y ==> x: thm

- decide_prenex ``!x. ?y. x /\ y``;
<<HOL message: HolQbfLib: calling external command
  'squolem2 -c /tmp/fileZAGj4m >/dev/null 2>&1'>>
> val it = [!x. ?y. x /\ y] |- F : thm

- disprove ``!x. ?y. x /\ y``;
<<HOL message: HolQbfLib: calling external command
  'squolem2 -c /tmp/file0Pw2Tg >/dev/null 2>&1'>>
> val it = [!x. ?y. x /\ y] |- F : thm

- prove ``?x. x``;
<<HOL message: HolQbfLib: calling external command
  'squolem2 -c /tmp/fileKi4Lkz >/dev/null 2>&1'>>
- val it =  [] |- ?x. x: thm

Supported subset of higher-order logic

The argument given to decide must be a Boolean term built using only conjunction, disjunction, implication, negation, universal/existential quantification, and variables. Free variables are considered universally quantified. Every quantified variable must occur.

The argument given to the other functions must be a QBF in prenex form, i.e., a term of the form $Q_1 x_1. \, Q_2 x_2. \, \ldots \, Q_n x_n. \, \phi$, where

  • $n \geq 0$,
  • each $Q_i$ is an (existential or universal) quantifier,
  • $Q_n$ is the existential quantifier,
  • each $x_i$ is a Boolean variable,
  • $\phi$ is a propositional formula in CNF, i.e., a conjunction of disjunctions of (possibly negated) Boolean variables,
  • $\phi$ must actually contain each $x_i$,
  • all $x_i$ must be distinct, and
  • $\phi$ does not contain variables other than $x_1, \ldots, x_n$.

The behavior is undefined if any of these restrictions are violated.

Support for the QDIMACS file format

The QDIMACS standard defines an input file format for QBF solvers. HolQbfLib provides a structure QDimacs that implements (parts of) the QDIMACS standard, version 1.1 (released on December 21, 2005), as described at http://www.qbflib.org/qdimacs.html. The QDimacs structure does not require Squolem (or any other QBF solver) to be installed.

QDimacs.write_qdimacs_file path $\phi$ creates a QDIMACS file (with name path) that encodes the QBF $\phi$, where $\phi$ must meet the requirements detailed above. The function returns a dictionary that maps each variable in $\phi$ to its corresponding variable index (a positive integer) used in the QDIMACS file.

QDimacs.read_qdimacs_file f path parses an existing QDIMACS file (with name path) and returns the encoded QBF as a HOL term. Since variables are only given as integers in the QDIMACS format, variables in HOL are obtained by applying f (which is a function of type int -> term) to each integer. f is expected to return Boolean variables only, not arbitrary HOL terms.

Tracing

Tracing output can be controlled via Feedback.set_trace "HolQbfLib". See the source code in QbfTrace.sml for possible values.

Communication between HOL and Squolem is via temporary files. These files are located in the standard temporary directory, typically /tmp on Unix machines. The actual file names are generated at run-time, and can be shown by setting the above tracing variable to a sufficiently high value.

The default behavior of HolQbfLib is to delete temporary files after successful invocation of Squolem. This also can be changed via the above tracing variable. If there is an error, files are retained in any case (but note that the operating system may delete temporary files automatically, e.g., when HOL exits).

Wishlist

The following features have not been implemented yet. Please submit additional feature requests (or code contributions) via http://github.com/HOL-Theorem-Prover/HOL.

Support for other QBF solvers

So far, Squolem is the only QBF solver that has been integrated with HOL. Several other QBF solvers can produce proofs, and it would be nice to offer HOL users more choice (also because Squolem's performance is not necessarily state-of-the-art anymore).

QBF solvers as a web service

The need to install a QBF solver locally poses an entry barrier. It would be much more convenient to have a web server running one (or several) QBF solvers, roughly similar to the “System on TPTP” interface that G. Sutcliffe provides for first-order theorem provers (http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP).