Abstract
Different theorem provers work within different formalisms and paradigms, and therefore produce various incompatible proof objects. Currently there is a big effort to establish foundational proof certificates (fpc), which would serve as a common “specification language” for all these formats. Such framework enables the uniform checking of proof objects from many different theorem provers while relying on a small and trusted kernel to do so. Checkers is an implementation of a proof checker using foundational proof certificates. By trusting a small kernel based on (focused) sequent calculus on the one hand and by supporting fpc specifications in a prolog-like language on the other hand, it can be used for checking proofs of a wide range of theorem provers. The focus of this paper is on the output of equational resolution theorem provers and for this end, we specify the paramodulation rule. We describe the architecture of Checkers and demonstrate how it can be used to check proof objects by supplying the fpc specification for a subset of the inferences used by eprover and checking proofs using these inferences.
Funded by the ERC Advanced Grant ProofCert.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Balint, A., Gall, D., Kapler, G., Retz, R.: Experiment design and administration for computer clusters for SAT-solvers (EDACC). JSAT (2010)
Boespflug, M., Carbonneaux, Q., Hermant, O.: The λΠ-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28–43 (2012)
Chihani, Z., Miller, D., Renaud, F.: Checking foundational proof certificates for first-order logic (extended abstract). In: Blanchette, J.C., Urban, J. (eds.) Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013). EPiC Series, vol. 14, pp. 58–66. EasyChair (2013)
Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 162–177. Springer, Heidelberg (2013)
Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a Nutshell. Journal of Formalized Reasoning 3(2), 153–245 (2010)
Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science 410(46), 4747–4768 (2009)
Miller, D.: Proofcert: Broad spectrum proof certificates, February 2011, an ERC Advanced Grant funded for the five years 2012-2016
Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, June 2012
Otten, J., Sutcliffe, G.: Using the tptp language for representing derivations in tableau and connection calculi. In: Schmidt, R.A., Schulz, S., Konev, B. (eds.) PAAR-2010. EPiC Series, vol. 9, pp. 95–105. EasyChair (2012)
Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Automation of Reasoning, pp. 298–313. Springer (1983)
Schulz, S.: System description: E 1.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 735–743. Springer, Heidelberg (2013)
Stump, A., Reynolds, A., Tinelli, C., Laugesen, A., Eades, H., Oliver, C., Zhang, R.: LFSC for SMT Proofs: Work in Progress
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Chihani, Z., Libal, T., Reis, G. (2015). The Proof Certifier Checkers . In: De Nivelle, H. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2015. Lecture Notes in Computer Science(), vol 9323. Springer, Cham. https://doi.org/10.1007/978-3-319-24312-2_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-24312-2_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24311-5
Online ISBN: 978-3-319-24312-2
eBook Packages: Computer ScienceComputer Science (R0)