\index{HolQbfLib|(}
\index{QBF|see {HolQbfLib}}
\index{Squolem|see {HolQbfLib}}
\index{decision procedures!QBF}

\setcounter{sessioncount}{0}

\ml{HolQbfLib} provides a rudimentary platform for experimenting with
combinations of theorem proving and Quantified Boolean Formulae~(QBF)
solvers.  \ml{HolQbfLib} was developed as part of a research project
on {\it Expressive Multi-theory Reasoning for Interactive
  Verification} (EPSRC grant EP/F067909/1) from 2008 to~2011.  It is
loosely inspired by \ml{HolSatLib} (Section~\ref{sec:HolSatLib}), and
has been described in parts in the following publications:
\begin{itemize}
\item Tjark Weber: {\it 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.
\item Ramana Kumar and Tjark Weber: {\it 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, volue 6898 of Lecture Notes in Computer Science, pages 168--183.
  Springer, 2011.
\end{itemize}
\ml{HolQbfLib} uses an external QBF solver, Squolem, to decide
Quantified Boolean Formulae.

\subsection{Installing Squolem}

\ml{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
\url{http://www.cprover.org/qbv/download.html}.  After installation,
you must make the executable available as {\tt squolem2}, \eg, by
placing it into a folder that is in your {\tt \$PATH}.  This name is
currently hard-coded: there is no configuration option to tell \HOL{}
about the location and name of the Squolem executable.

\subsection{Interface}
\label{qbf-interface}

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

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

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

\ml{decide\_prenex $\phi$} combines the functionality of \ml{prove} and
\ml{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, \ml{decide} does the same job as \ml{decide\_prenex} but accepts QBFs
in a less restricted form. Restrictions on $\phi$ are described below.

\begin{figure}
\begin{session}
\begin{verbatim}
- 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
\end{verbatim}
\end{session}
\caption{\ml{HolQbfLib} in action.}
\end{figure}

\paragraph{Supported subset of higher-order logic}
The argument given to \ml{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, \ie, a term of the form $Q_1 x_1. \, Q_2 x_2. \, \ldots
\, Q_n x_n. \, \phi$, where
\begin{itemize}
\item $n \geq 0$,
\item each $Q_i$ is an (existential or universal) quantifier,
\item $Q_n$ is the existential quantifier,
\item each $x_i$ is a Boolean variable,
\item $\phi$ is a propositional formula in CNF, \ie, a conjunction of
  disjunctions of (possibly negated) Boolean variables,
\item $\phi$ must actually contain each $x_i$,
\item all $x_i$ must be distinct, and
\item $\phi$ does not contain variables other than $x_1$, \dots,
  $x_n$.
\end{itemize}
The behavior is undefined if any of these restrictions are violated.

\paragraph{Support for the QDIMACS file format}

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

\ml{QDimacs.write\_qdimacs\_file path $\phi$} creates a QDIMACS file
(with name \ml{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.

\ml{QDimacs.read\_qdimacs\_file f path} parses an existing QDIMACS
file (with name \ml{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 \ml{f} (which is
a function of type \ml{int -> term}) to each integer.  \ml{f} is
expected to return Boolean variables only, not arbitrary \HOL{} terms.

\paragraph{Tracing}

Tracing output can be controlled via \ml{Feedback.set\_trace
  "HolQbfLib"}.  See the source code in \ml{QbfTrace.sml} for possible
values.

Communication between \HOL{} and Squolem is via temporary files.
These files are located in the standard temporary directory, typically
{\tt /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 \ml{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, \eg, when \HOL{} exits).

\subsection{Wishlist}

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

\paragraph{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).

\paragraph{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
(\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}).

\index{HolQbfLib|)}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "description"
%%% End: