Tjark Weber. 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.
The Quantified Boolean Formulae (QBF) solver Squolem can generate certificates of invalidity, based on Q-resolution. We present independent checking of these certificates in the HOL4 theorem prover. This enables HOL4 users to benefit from Squolem's automation for QBF problems, and provides high correctness assurances for Squolem's results. Detailed performance data shows that LCF-style certificate checking is feasible even for large QBF instances. Our work prompted improvements to HOL4's inference kernel.
The original publication is available at www.springerlink.com.
@inproceedings{weber10validating,
author = {Tjark Weber},
title = {Validating {QBF} Invalidity in {HOL4}},
editor = {Matt Kaufmann and Lawrence C. Paulson},
booktitle = {Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July~11-14, 2010. Proceedings},
volume = {6172},
series = {Lecture Notes in Computer Science},
pages = {466--480},
publisher = {Springer},
year = {2010},
url = {http://dx.doi.org/10.1007/978-3-642-14052-5_32}
}
QBF benchmarks and detailed evaluation data are available here (107 MB).