{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,23]],"date-time":"2026-02-23T23:09:52Z","timestamp":1771888192550,"version":"3.50.1"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319243115","type":"print"},{"value":"9783319243122","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_14","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T14:06:46Z","timestamp":1441894006000},"page":"201-210","source":"Crossref","is-referenced-by-count":11,"title":["The Proof Certifier Checkers"],"prefix":"10.1007","author":[{"given":"Zakaria","family":"Chihani","sequence":"first","affiliation":[]},{"given":"Tomer","family":"Libal","sequence":"additional","affiliation":[]},{"given":"Giselle","family":"Reis","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Balint, A., Gall, D., Kapler, G., Retz, R.: Experiment design and administration for computer clusters for SAT-solvers (EDACC). JSAT (2010)","DOI":"10.3233\/SAT190078"},{"key":"14_CR2","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The \u03bb\u03a0-calculus modulo as a universal proof language. In: Pichardie, D., Weber, T. (eds.) Proceedings of PxTP2012: Proof Exchange for Theorem Proving, pp. 28\u201343 (2012)"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"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.\u00a014, pp. 58\u201366. EasyChair (2013)","DOI":"10.29007\/7gnr"},{"key":"14_CR4","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-38574-2_11","volume-title":"Automated Deduction \u2013 CADE-24","author":"Z. Chihani","year":"2013","unstructured":"Chihani, Z., Miller, D., Renaud, F.: Foundational proof certificates in first-order logic. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol.\u00a07898, pp. 162\u2013177. Springer, Heidelberg (2013)"},{"issue":"2","key":"14_CR5","first-page":"153","volume":"3","author":"A. Grabowski","year":"2010","unstructured":"Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a Nutshell. Journal of Formalized Reasoning\u00a03(2), 153\u2013245 (2010)","journal-title":"Journal of Formalized Reasoning"},{"issue":"46","key":"14_CR6","doi-asserted-by":"publisher","first-page":"4747","DOI":"10.1016\/j.tcs.2009.07.041","volume":"410","author":"C. Liang","year":"2009","unstructured":"Liang, C., Miller, D.: Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science\u00a0410(46), 4747\u20134768 (2009)","journal-title":"Theoretical Computer Science"},{"key":"14_CR7","unstructured":"Miller, D.: Proofcert: Broad spectrum proof certificates, February 2011, an ERC Advanced Grant funded for the five years 2012-2016"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press, June 2012","DOI":"10.1017\/CBO9781139021326"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"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.\u00a09, pp. 95\u2013105. EasyChair (2012)","DOI":"10.29007\/jcqn"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Robinson, G., Wos, L.: Paramodulation and theorem-proving in first-order theories with equality. In: Automation of Reasoning, pp. 298\u2013313. Springer (1983)","DOI":"10.1007\/978-3-642-81955-1_19"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"735","DOI":"10.1007\/978-3-642-45221-5_49","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"S. Schulz","year":"2013","unstructured":"Schulz, S.: System description: E\u00a01.8. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol.\u00a08312, pp. 735\u2013743. Springer, Heidelberg (2013)"},{"key":"14_CR12","unstructured":"Stump, A., Reynolds, A., Tinelli, C., Laugesen, A., Eades, H., Oliver, C., Zhang, R.: LFSC for SMT Proofs: Work in Progress"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T14:54:37Z","timestamp":1748616877000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}