Ramana Kumar and Tjark Weber. 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.
The Quantified Boolean Formulae (QBF) solver Squolem can generate certificates of validity, based on Skolem functions. We present independent checking of these certificates in the HOL4 theorem prover. This enables HOL4 users to benefit from Squolem's automation for valid QBF problems. Detailed performance data shows that LCF-style checking of validity certificates is often (but not always) feasible even for large QBF instances. Additionally, our work provides high correctness assurances for Squolem's claims of validity and uncovered a soundness bug in a previous version of its certificate validator QBV.
The original publication is available at www.springerlink.com.
@inproceedings{kumar11validating,
author = {Ramana Kumar and Tjark Weber},
title = {Validating {QBF} Validity in {HOL4}},
editor = {van Eekelen, Marko C. J. D. and Herman Geuvers and Julien Schmaltz and Freek Wiedijk},
booktitle = {Interactive Theorem Proving - Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August~22-25, 2011. Proceedings},
volume = {6898},
series = {Lecture Notes in Computer Science},
pages = {168--183},
publisher = {Springer},
year = {2011}
}
For evaluation, we used the preliminary2006 (103 MB) set of 425 QBF benchmarks.
Our experimental results are tabulated here.
To generate certificates of (in)validity, we applied Squolem 2.02 to the preliminary2006 benchmark set, using a timeout of 600 s per benchmark. The resulting certificates and detailed timing data for Squolem are available here (7 MB).
To compare the performance of HOL4 to that of Squolem's certificate checker QBV, we applied QBV 2.0 to all 100 certificates of validity that were generated by Squolem. A log file with timing data is available here (4 kB).
Detailed evaluation data for HOL4 (again including the preliminary2006 benchmarks and Squolem's certificates for them) are available here (109 MB).