{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,5]],"date-time":"2026-10-05T20:53:50Z","timestamp":1791233630574,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642452208","type":"print"},{"value":"9783642452215","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-45221-5_20","type":"book-chapter","created":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T09:28:23Z","timestamp":1386235703000},"page":"274-290","source":"Crossref","is-referenced-by-count":24,"title":["Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo"],"prefix":"10.1007","author":[{"given":"David","family":"Delahaye","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damien","family":"Doligez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Fr\u00e9d\u00e9ric","family":"Gilbert","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pierre","family":"Halmagrand","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Olivier","family":"Hermant","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book, Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996) ISBN\u00a00521496195","DOI":"10.1017\/CBO9780511624162"},{"key":"20_CR2","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The \u03bb\u03a0-Calculus Modulo as a Universal Proof Language. In: Pichardie, D., Weber, T. (eds.) Proof Exchange for Theorem Proving (PxTP), Manchester, UK, pp. 28\u201343 (June 2012)"},{"key":"20_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-540-25984-8_33","volume-title":"Automated Reasoning","author":"R. Bonichon","year":"2004","unstructured":"Bonichon, R.: TaMeD: A Tableau Method for Deduction Modulo. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 445\u2013459. Springer, Heidelberg (2004)"},{"key":"20_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75560-9_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Bonichon","year":"2007","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 151\u2013165. Springer, Heidelberg (2007)"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Brauner, P., Houtmann, C., Kirchner, C.: Principles of Superdeduction. In: Logic in Computer Science (LICS), Wroc\u0142aw, Poland, pp. 41\u201350. IEEE Computer Society Press (July 2007)","DOI":"10.1109\/LICS.2007.37"},{"issue":"1","key":"20_CR6","first-page":"1","volume":"7","author":"G. Burel","year":"2011","unstructured":"Burel, G.: Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo. Logical Methods in Computer Science (LMCS)\u00a07(1), 1\u201331 (2011)","journal-title":"Logical Methods in Computer Science (LMCS)"},{"key":"20_CR7","series-title":"LNCS (LNAI)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-22438-6_14","volume-title":"Automated Deduction \u2013 CADE-23","author":"G. Burel","year":"2011","unstructured":"Burel, G.: Experimenting with Deduction Modulo. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 162\u2013176. Springer, Heidelberg (2011)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-45841-7_3","volume-title":"STACS 2002","author":"G. Dowek","year":"2002","unstructured":"Dowek, G.: What is a Theory? In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol.\u00a02285, pp. 50\u201364. Springer, Heidelberg (2002)"},{"issue":"1","key":"20_CR9","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem Proving Modulo. Journal of Automated Reasoning (JAR)\u00a031(1), 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-642-31365-3_26","volume-title":"Automated Reasoning","author":"M. Jacquel","year":"2012","unstructured":"Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Tableaux Modulo Theories using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol.\u00a07364, pp. 332\u2013338. Springer, Heidelberg (2012)"},{"key":"20_CR11","unstructured":"Prawitz, D.: Natural Deduction. A Proof-Theoretical Study. Stockholm Studies in Philosophy\u00a03 (1965)"},{"issue":"4","key":"20_CR12","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G. Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP Problem Library and Associated Infrastructure: The FOF and CNF Parts, v3.5.0. Journal of Automated Reasoning (JAR)\u00a043(4), 337\u2013362 (2009)","journal-title":"Journal of Automated Reasoning (JAR)"},{"key":"20_CR13","unstructured":"The BWare Project (2012), \n                  \n                    http:\/\/bware.lri.fr\/"},{"key":"20_CR14","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge University Press, Cambridge (1996) ISBN\u00a00521779111"},{"key":"20_CR15","unstructured":"Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics: An Introduction. Elsevier, Amsterdam (1988) ISBN\u00a00444705066"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming, Artificial Intelligence, and Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-45221-5_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T04:38:47Z","timestamp":1558759127000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-45221-5_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642452208","9783642452215"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-45221-5_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}