Abstract
We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications produced by Focal. Zenon can also be extended, which makes specific (and possibly local) automation possible in Focal.
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
Barendregt, H., Barendsen, E.: Autarkic Computations in Formal Proofs. Journal of Automated Reasoning (JAR) 28(3), 321–336 (2002)
Bezem, M., Hendriks, D.H., de Nivelle, H.: Automated Proof Construction in Type Theory Using Resolution. Journal of Automated Reasoning (JAR) 29(3–4), 253–275 (2002)
Delahaye, D., Étienne, J.-F., Donzeau-Gouge, V.V.: Certifying Airport Security Regulations using the Focal Environment. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 48–63. Springer, Heidelberg (2006)
Delahaye, D., Étienne, J.-F., Donzeau-Gouge, V.V.: Reasoning about Airport Security Regulations using the Focal Environment. In: International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA), Paphos (Cyprus) (November 2006)
Hurd, J.: Integrating Gandal and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 311–322. Springer, Heidelberg (1999)
Jaume, M., Morisset, C.: Formalisation and Implementation of Access Control Models. In: Information Assurance and Security (IAS), International Conference on Information Technology (ITCC), Las Vegas (USA), pp. 703–708. IEEE Computer Society Press, Los Alamitos (2005)
Leisenring, A.C.: Mathematical Logic and Hilbert’s ε-Symbol. MacDonald Technical and Scientific, London (1969) ISBN 0356026795
McCune, W., Shumsky, O.: System Description: IVY. In: McAllester, D. (ed.) CADE-17. LNCS, vol. 1831, pp. 401–405. Springer, Heidelberg (2000)
Paulson, L.C., Susanto, K.W.: Source-Level Proof Reconstruction for Interactive Theorem Proving. In: Theorem Proving in Higher Order Logics (TPHOLs). LNCS, Springer, Heidelberg (2007)
The EDEMOI Project (2003), http://www-lsr.imag.fr/EDEMOI/
Sutcliffe, G.: CASC-J3 - The 3rd IJCAR ATP System Competition. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 572–573. Springer, Heidelberg (2006)
Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning (JAR) 21(2), 177–203 (1998)
The Coq Development Team. Coq, version 8.1. INRIA (November 2006), available at: http://coq.inria.fr/
The Cristal Team. Objective Caml, version 3.10. INRIA (May 2007), available at: http://caml.inria.fr/
The Focal Development Team. Focal, version 0.3.1. CNAM/INRIA/LIP6 (May 2005), available at: http://focal.inria.fr/
The HELM Team. Matita, version 0.1.0. Computer Science Department, University of Bologna (July 2006), available at: http://matita.cs.unibo.it/
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bonichon, R., Delahaye, D., Doligez, D. (2007). Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs. In: Dershowitz, N., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2007. Lecture Notes in Computer Science(), vol 4790. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75560-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-75560-9_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75558-6
Online ISBN: 978-3-540-75560-9
eBook Packages: Computer ScienceComputer Science (R0)