×

A modular integration of SAT/SMT solvers to Coq through proof witnesses. (English) Zbl 1350.68223

Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 135-150 (2011).
Summary: We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs’ complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq’s logic by calling external provers and carefully checking their answers.
For the entire collection see [Zbl 1226.68005].

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Source code of the development, http://www.lix.polytechnique.fr/ keller/Recherche/smtcoq.html
[2] SMT-LIB, http://www.smtlib.org
[3] Armand, M., Grégoire, B., Spiwack, A., Théry, L.: Extending Coq with Imperative Features and Its Application to SAT Verification. In: Kaufmann and Paulson [9], pp. 83–98 · Zbl 1291.68318 · doi:10.1007/978-3-642-14052-5_8
[4] Barendregt, H., Barendsen, E.: Autarkic Computations in Formal Proofs. J. Autom. Reasoning 28(3), 321–336 (2002) · Zbl 1002.68156 · doi:10.1023/A:1015761529444
[5] Besson, F.: Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol. 4502, pp. 48–62. Springer, Heidelberg (2007) · Zbl 1178.03020 · doi:10.1007/978-3-540-74464-1_4
[6] Böhme, S., Weber, T.: Fast LCF-Style Proof Reconstruction for Z3. In: Kaufmann and Paulson [9], pp. 179–194 · Zbl 1291.68328 · doi:10.1007/978-3-642-14052-5_14
[7] Dénès, M.: Coq with native compilation, https://github.com/maximedenes/native-coq
[8] Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.F.: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006) · Zbl 1180.68240 · doi:10.1007/11691372_11
[9] Kaufmann, M., Paulson, L.C. (eds.): ITP 2010. LNCS, vol. 6172. Springer, Heidelberg (2010) · Zbl 1195.68009
[10] Lescuyer, S., Conchon, S.: Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme. In: Ghilardi, S., Sebastiani, R. (eds.) FroCoS 2009. LNCS, vol. 5749, pp. 287–303. Springer, Heidelberg (2009) · Zbl 1193.68225 · doi:10.1007/978-3-642-04222-5_18
[11] McLaughlin, S., Barrett, C., Ge, Y.: Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. ENTCS 144(2), 43–51 (2006) · Zbl 1272.68362
[12] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL. J. ACM 53(6), 937–977 (2006) · Zbl 1326.68164 · doi:10.1145/1217856.1217859
[13] Oe, D., Stump, A.: Extended Abstract: Combining a Logical Framework with an RUP Checker for SMT Proofs. In: Lahiri, S., Seshia, S. (eds.) Proceedings of the 9th International Workshop on Satisfiability Modulo Theories, Snowbird, USA (2011)
[14] Tseitin, G.S.: On the complexity of proofs in propositional logics. Automation of Reasoning: Classical Papers in Computational Logic (1967-1970) 2 (1983)
[15] Weber, T.: SAT-based Finite Model Generation for Higher-Order Logic. Ph.D. thesis, Institut für Informatik, Technische Universität München, Germany (April 2008), http://www.cl.cam.ac.uk/ tw333/publications/weber08satbased.html
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.