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{session} 69\begin{verbatim} 70- load "HolQbfLib"; 71metis: r[+0+3]# 72r[+0+6]# 73> val it = () : unit 74 75- open HolQbfLib; 76> val decide = fn: term -> thm 77val decide_prenex = fn: term -> thm 78val disprove = fn: term -> thm 79val prove = fn: term -> thm 80 81- show_assums := true; 82> val it = () : unit 83 84- decide ``?x. x``; 85<<HOL message: HolQbfLib: calling external command 86 'squolem2 -c /tmp/filedH1K2x >/dev/null 2>&1'>> 87> val it = [] |- ?x. x: thm 88 89- decide ``(?y. x \/ y) ==> ~x``; 90> val it = [!x. (?y. x \/ y) ==> ~x] |- F: thm 91 92- decide ``~(?x. x ==> y) \/ (?x. y ==> x)``; 93<<HOL message: HolQbfLib: calling external command 94 'squolem2 -c /tmp/fileyap3oD >/dev/null 2>&1'>> 95> val it = [] |- ~(?x. x ==> y) \/ ?x. y ==> x: thm 96 97- decide_prenex ``!x. ?y. x /\ y``; 98<<HOL message: HolQbfLib: calling external command 99 'squolem2 -c /tmp/fileZAGj4m >/dev/null 2>&1'>> 100> val it = [!x. ?y. x /\ y] |- F : thm 101 102- disprove ``!x. ?y. x /\ y``; 103<<HOL message: HolQbfLib: calling external command 104 'squolem2 -c /tmp/file0Pw2Tg >/dev/null 2>&1'>> 105> val it = [!x. ?y. x /\ y] |- F : thm 106 107- prove ``?x. x``; 108<<HOL message: HolQbfLib: calling external command 109 'squolem2 -c /tmp/fileKi4Lkz >/dev/null 2>&1'>> 110- val it = [] |- ?x. x: thm 111\end{verbatim} 112\end{session} 113 114\paragraph{Supported subset of higher-order logic} 115The 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. 116 117The argument given to the other functions must be a QBF in 118prenex form, \ie, a term of the form $Q_1 x_1. \, Q_2 x_2. \, \ldots 119\, Q_n x_n. \, \phi$, where 120\begin{itemize} 121\item $n \geq 0$, 122\item each $Q_i$ is an (existential or universal) quantifier, 123\item $Q_n$ is the existential quantifier, 124\item each $x_i$ is a Boolean variable, 125\item $\phi$ is a propositional formula in CNF, \ie, a conjunction of 126 disjunctions of (possibly negated) Boolean variables, 127\item $\phi$ must actually contain each $x_i$, 128\item all $x_i$ must be distinct, and 129\item $\phi$ does not contain variables other than $x_1$, \dots, 130 $x_n$. 131\end{itemize} 132The behavior is undefined if any of these restrictions are violated. 133 134\paragraph{Support for the QDIMACS file format} 135 136The QDIMACS standard defines an input file format for QBF solvers. 137\ml{HolQbfLib} provides a structure \ml{QDimacs} that implements 138(parts of) the QDIMACS standard, version 1.1 (released on December~21, 1392005), as described at \url{http://www.qbflib.org/qdimacs.html}. The 140\ml{QDimacs} structure does not require Squolem (or any other QBF 141solver) to be installed. 142 143\ml{QDimacs.write\_qdimacs\_file path $\phi$} creates a QDIMACS file 144(with name \ml{path}) that encodes the QBF $\phi$, where $\phi$ must 145meet the requirements detailed above. The function returns a 146dictionary that maps each variable in~$\phi$ to its corresponding 147variable index (a positive integer) used in the QDIMACS file. 148 149\ml{QDimacs.read\_qdimacs\_file f path} parses an existing QDIMACS 150file (with name \ml{path}) and returns the encoded QBF as a \HOL{} 151term. Since variables are only given as integers in the QDIMACS 152format, variables in \HOL{} are obtained by applying \ml{f} (which is 153a function of type \ml{int -> term}) to each integer. \ml{f} is 154expected to return Boolean variables only, not arbitrary \HOL{} terms. 155 156\paragraph{Tracing} 157 158Tracing output can be controlled via \ml{Feedback.set\_trace 159 "HolQbfLib"}. See the source code in \ml{QbfTrace.sml} for possible 160values. 161 162Communication between \HOL{} and Squolem is via temporary files. 163These files are located in the standard temporary directory, typically 164{\tt /tmp} on Unix machines. The actual file names are generated at 165run-time, and can be shown by setting the above tracing variable to a 166sufficiently high value. 167 168The default behavior of \ml{HolQbfLib} is to delete temporary files 169after successful invocation of Squolem. This also can be changed via 170the above tracing variable. If there is an error, files are retained 171in any case (but note that the operating system may delete temporary 172files automatically, \eg, when \HOL{} exits). 173 174\subsection{Wishlist} 175 176The following features have not been implemented yet. 177Please submit additional feature requests (or code contributions) via \url{http://github.com/mn200/HOL}. 178 179\paragraph{Support for other QBF solvers} 180 181So far, Squolem is the only QBF solver that has been integrated with 182\HOL. Several other QBF solvers can produce proofs, and it would be 183nice to offer \HOL{} users more choice (also because Squolem's 184performance is not necessarily state-of-the-art anymore). 185 186\paragraph{QBF solvers as a web service} 187 188The need to install a QBF solver locally poses an entry barrier. It 189would be much more convenient to have a web server running one (or 190several) QBF solvers, roughly similar to the ``System on TPTP'' 191interface that G.~Sutcliffe provides for first-order theorem provers 192(\url{http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP}). 193 194\index{HolQbfLib|)} 195 196%%% Local Variables: 197%%% mode: latex 198%%% TeX-master: "description" 199%%% End: 200