1\index{HolQbfLib|(} 2\index{QBF|see {HolQbfLib}} 3\index{Squolem|see {HolQbfLib}} 4\index{decision procedures!QBF} 5 6\setcounter{sessioncount}{0} 7 8\ml{HolQbfLib} provides a rudimentary platform for experimenting with 9combinations of theorem proving and Quantified Boolean Formulae~(QBF) 10solvers. \ml{HolQbfLib} was developed as part of a research project 11on {\it Expressive Multi-theory Reasoning for Interactive 12 Verification} (EPSRC grant EP/F067909/1) from 2008 to~2011. It is 13loosely inspired by \ml{HolSatLib} (Section~\ref{sec:HolSatLib}), and 14has been described in parts in the following publications: 15\begin{itemize} 16\item Tjark Weber: {\it Validating QBF Invalidity in HOL4}. In Matt 17 Kaufmann and Lawrence C.\ Paulson, editors, Interactive Theorem 18 Proving, First International Conference, ITP 2010, Edinburgh, UK, 19 July 11--14, 2010. Proceedings, volume 6172 of Lecture Notes in 20 Computer Science, pages 466--480. Springer, 2010. 21\item Ramana Kumar and Tjark Weber: {\it Validating QBF Validity in 22 HOL4}. In Marko C.\ J.\ D.\ van Eekelen, Herman Geuvers, Julien Schmaltz, 23 and Freek Wiedijk, editors, Interactive Theorem Proving, Second International 24 Conference, ITP 2011, Berg en Dal, The Netherlands, August 22--25, 2011. 25 Proceedings, volue 6898 of Lecture Notes in Computer Science, pages 168--183. 26 Springer, 2011. 27\end{itemize} 28\ml{HolQbfLib} uses an external QBF solver, Squolem, to decide 29Quantified Boolean Formulae. 30 31\subsection{Installing Squolem} 32 33\ml{HolQbfLib} has been tested with (the x86 Linux version of) Squolem 342.02 (release date 2010-11-10). This is Squolem's latest version at 35the time of writing. Squolem can be obtained from 36\url{http://www.cprover.org/qbv/download.html}. After installation, 37you must make the executable available as {\tt squolem2}, \eg, by 38placing it into a folder that is in your {\tt \$PATH}. This name is 39currently hard-coded: there is no configuration option to tell \HOL{} 40about the location and name of the Squolem executable. 41 42\subsection{Interface} 43\label{qbf-interface} 44 45The library provides four functions, each of type \ml{term -> thm}, to invoke 46Squolem: \ml{decide}, \ml{decide\_prenex}, \ml{disprove}, and \ml{prove}. These 47are defined in the \ml{HolQbfLib} structure, which is the library's main entry 48point. 49 50Calling \ml{prove $\phi$} will invoke Squolem on the QBF~$\phi$ to 51establish its validity. If this succeeds, \ml{prove} will then 52validate the certificate of validity generated by Squolem in \HOL{} to 53return a theorem $\vdash \phi$. 54 55Similarly, calling \ml{disprove $\phi$} will invoke Squolem to 56establish that $\phi$ is invalid. If this succeeds, \ml{disprove} 57will then validate the certificate of invalidity generated by Squolem 58in \HOL{} to return a theorem $\phi \vdash \bot$. 59 60\ml{decide\_prenex $\phi$} combines the functionality of \ml{prove} and 61\ml{disprove} into a single function. It will invoke Squolem on 62$\phi$ and return either $\vdash \phi$ or $\phi \vdash \bot$, 63depending on Squolem's answer. 64 65Finally, \ml{decide} does the same job as \ml{decide\_prenex} but accepts QBFs 66in a less restricted form. Restrictions on $\phi$ are described below. 67 68\begin{figure} 69\begin{session} 70\begin{verbatim} 71- load "HolQbfLib"; 72metis: r[+0+3]# 73r[+0+6]# 74> val it = () : unit 75 76- open HolQbfLib; 77> val decide = fn: term -> thm 78val decide_prenex = fn: term -> thm 79val disprove = fn: term -> thm 80val prove = fn: term -> thm 81 82- show_assums := true; 83> val it = () : unit 84 85- decide ``?x. x``; 86<<HOL message: HolQbfLib: calling external command 87 'squolem2 -c /tmp/filedH1K2x >/dev/null 2>&1'>> 88> val it = [] |- ?x. x: thm 89 90- decide ``(?y. x \/ y) ==> ~x``; 91> val it = [!x. (?y. x \/ y) ==> ~x] |- F: thm 92 93- decide ``~(?x. x ==> y) \/ (?x. y ==> x)``; 94<<HOL message: HolQbfLib: calling external command 95 'squolem2 -c /tmp/fileyap3oD >/dev/null 2>&1'>> 96> val it = [] |- ~(?x. x ==> y) \/ ?x. y ==> x: thm 97 98- decide_prenex ``!x. ?y. x /\ y``; 99<<HOL message: HolQbfLib: calling external command 100 'squolem2 -c /tmp/fileZAGj4m >/dev/null 2>&1'>> 101> val it = [!x. ?y. x /\ y] |- F : thm 102 103- disprove ``!x. ?y. x /\ y``; 104<<HOL message: HolQbfLib: calling external command 105 'squolem2 -c /tmp/file0Pw2Tg >/dev/null 2>&1'>> 106> val it = [!x. ?y. x /\ y] |- F : thm 107 108- prove ``?x. x``; 109<<HOL message: HolQbfLib: calling external command 110 'squolem2 -c /tmp/fileKi4Lkz >/dev/null 2>&1'>> 111- val it = [] |- ?x. x: thm 112\end{verbatim} 113\end{session} 114\caption{\ml{HolQbfLib} in action.} 115\end{figure} 116 117\paragraph{Supported subset of higher-order logic} 118The 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. 119 120The argument given to the other functions must be a QBF in 121prenex form, \ie, a term of the form $Q_1 x_1. \, Q_2 x_2. \, \ldots 122\, Q_n x_n. \, \phi$, where 123\begin{itemize} 124\item $n \geq 0$, 125\item each $Q_i$ is an (existential or universal) quantifier, 126\item $Q_n$ is the existential quantifier, 127\item each $x_i$ is a Boolean variable, 128\item $\phi$ is a propositional formula in CNF, \ie, a conjunction of 129 disjunctions of (possibly negated) Boolean variables, 130\item $\phi$ must actually contain each $x_i$, 131\item all $x_i$ must be distinct, and 132\item $\phi$ does not contain variables other than $x_1$, \dots, 133 $x_n$. 134\end{itemize} 135The behavior is undefined if any of these restrictions are violated. 136 137\paragraph{Support for the QDIMACS file format} 138 139The QDIMACS standard defines an input file format for QBF solvers. 140\ml{HolQbfLib} provides a structure \ml{QDimacs} that implements 141(parts of) the QDIMACS standard, version 1.1 (released on December~21, 1422005), as described at \url{http://www.qbflib.org/qdimacs.html}. The 143\ml{QDimacs} structure does not require Squolem (or any other QBF 144solver) to be installed. 145 146\ml{QDimacs.write\_qdimacs\_file path $\phi$} creates a QDIMACS file 147(with name \ml{path}) that encodes the QBF $\phi$, where $\phi$ must 148meet the requirements detailed above. The function returns a 149dictionary that maps each variable in~$\phi$ to its corresponding 150variable index (a positive integer) used in the QDIMACS file. 151 152\ml{QDimacs.read\_qdimacs\_file f path} parses an existing QDIMACS 153file (with name \ml{path}) and returns the encoded QBF as a \HOL{} 154term. Since variables are only given as integers in the QDIMACS 155format, variables in \HOL{} are obtained by applying \ml{f} (which is 156a function of type \ml{int -> term}) to each integer. \ml{f} is 157expected to return Boolean variables only, not arbitrary \HOL{} terms. 158 159\paragraph{Tracing} 160 161Tracing output can be controlled via \ml{Feedback.set\_trace 162 "HolQbfLib"}. See the source code in \ml{QbfTrace.sml} for possible 163values. 164 165Communication between \HOL{} and Squolem is via temporary files. 166These files are located in the standard temporary directory, typically 167{\tt /tmp} on Unix machines. The actual file names are generated at 168run-time, and can be shown by setting the above tracing variable to a 169sufficiently high value. 170 171The default behavior of \ml{HolQbfLib} is to delete temporary files 172after successful invocation of Squolem. This also can be changed via 173the above tracing variable. If there is an error, files are retained 174in any case (but note that the operating system may delete temporary 175files automatically, \eg, when \HOL{} exits). 176 177\subsection{Wishlist} 178 179The following features have not been implemented yet. 180Please submit additional feature requests (or code contributions) via \url{http://github.com/HOL-Theorem-Prover/HOL}. 181 182\paragraph{Support for other QBF solvers} 183 184So far, Squolem is the only QBF solver that has been integrated with 185\HOL. Several other QBF solvers can produce proofs, and it would be 186nice to offer \HOL{} users more choice (also because Squolem's 187performance is not necessarily state-of-the-art anymore). 188 189\paragraph{QBF solvers as a web service} 190 191The need to install a QBF solver locally poses an entry barrier. It 192would be much more convenient to have a web server running one (or 193several) QBF solvers, roughly similar to the ``System on TPTP'' 194interface that G.~Sutcliffe provides for first-order theorem provers 195(\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}). 196 197\index{HolQbfLib|)} 198 199%%% Local Variables: 200%%% mode: latex 201%%% TeX-master: "description" 202%%% End: 203