{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T05:50:40Z","timestamp":1791352240996,"version":"4.3.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540755586","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75560-9_13","type":"book-chapter","created":{"date-parts":[[2007,10,6]],"date-time":"2007-10-06T05:36:46Z","timestamp":1191649006000},"page":"151-165","source":"Crossref","is-referenced-by-count":69,"title":["Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bonichon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"Delahaye","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damien","family":"Doligez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"3","key":"13_CR1","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic Computations in Formal Proofs. Journal of Automated Reasoning (JAR)\u00a028(3), 321\u2013336 (2002)","journal-title":"Journal of Automated Reasoning (JAR)"},{"issue":"3\u20134","key":"13_CR2","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1023\/A:1021939521172","volume":"29","author":"M. Bezem","year":"2002","unstructured":"Bezem, M., Hendriks, D.H., de Nivelle, H.: Automated Proof Construction in Type Theory Using Resolution. Journal of Automated Reasoning (JAR)\u00a029(3\u20134), 253\u2013275 (2002)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11813040_4","volume-title":"FM 2006: Formal Methods","author":"D. Delahaye","year":"2006","unstructured":"Delahaye, D., \u00c9tienne, 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.\u00a04085, pp. 48\u201363. Springer, Heidelberg (2006)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Delahaye, D., \u00c9tienne, 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)","DOI":"10.1109\/ISoLA.2006.25"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"Hurd, J.: Integrating Gandal and HOL. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 311\u2013322. Springer, Heidelberg (1999)"},{"key":"13_CR6","first-page":"703","volume-title":"Information Assurance and Security (IAS), International Conference on Information Technology (ITCC)","author":"M. Jaume","year":"2005","unstructured":"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\u2013708. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"13_CR7","unstructured":"Leisenring, A.C.: Mathematical Logic and Hilbert\u2019s \u03b5-Symbol. MacDonald Technical and Scientific, London (1969) ISBN 0356026795"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/10721959_30","volume-title":"CADE-17","author":"W. McCune","year":"2000","unstructured":"McCune, W., Shumsky, O.: System Description: IVY. In: McAllester, D. (ed.) CADE-17. LNCS, vol.\u00a01831, pp. 401\u2013405. Springer, Heidelberg (2000)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs)","author":"L.C. Paulson","year":"2007","unstructured":"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)"},{"key":"13_CR10","unstructured":"The\u00a0 EDEMOI Project (2003), \n                  \n                    http:\/\/www-lsr.imag.fr\/EDEMOI\/"},{"key":"13_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1007\/11814771_46","volume-title":"Automated Reasoning","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G.: CASC-J3 - The 3\n                  rd\n                 IJCAR ATP System Competition. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 572\u2013573. Springer, Heidelberg (2006)"},{"issue":"2","key":"13_CR12","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning (JAR)\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"13_CR13","unstructured":"The Coq\u00a0Development Team. Coq, version\u00a08.1. INRIA (November 2006), available at: \n                  \n                    http:\/\/coq.inria.fr\/"},{"key":"13_CR14","unstructured":"The\u00a0Cristal Team. Objective Caml, version\u00a03.10. INRIA (May 2007), available at: \n                  \n                    http:\/\/caml.inria.fr\/"},{"key":"13_CR15","unstructured":"The Focal\u00a0Development Team. Focal, version 0.3.1. CNAM\/INRIA\/LIP6 (May 2005), available at: \n                  \n                    http:\/\/focal.inria.fr\/"},{"key":"13_CR16","unstructured":"The\u00a0HELM Team. Matita, version 0.1.0. Computer Science Department, University of Bologna (July 2006), available at: \n                  \n                    http:\/\/matita.cs.unibo.it\/"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75560-9_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:24:39Z","timestamp":1619519079000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75560-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540755586"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75560-9_13","relation":{},"subject":[]}}