{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T22:51:17Z","timestamp":1776552677362,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540280057","type":"print"},{"value":"9783540318644","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_7","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"84-98","source":"Crossref","is-referenced-by-count":5,"title":["The CoRe Calculus"],"prefix":"10.1007","author":[{"given":"Serge","family":"Autexier","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"7_CR1","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1016\/S0168-0072(00)00032-4","volume":"107","author":"J.-M. Andreoli","year":"2000","unstructured":"Andreoli, J.-M.: Focusing and proof construction. Annals of Pure and Applied Logic\u00a0107(1), 131\u2013163 (2000)","journal-title":"Annals of Pure and Applied Logic"},{"issue":"2","key":"7_CR2","doi-asserted-by":"publisher","first-page":"385","DOI":"10.2307\/2272981","volume":"37","author":"P.B. Andrews","year":"1972","unstructured":"Andrews, P.B.: General models, descriptions, and choice in type theory. The Journal of Symbolic Logic\u00a037(2), 385\u2013397 (1972)","journal-title":"The Journal of Symbolic Logic"},{"key":"7_CR3","unstructured":"Autexier, S.: Hierarchical Contextual Reasoning. PhD thesis, Computer Science Department, Saarland University, Saarbr\u00fccken, Germany (2003)"},{"key":"7_CR4","volume-title":"The \u03bb-Calculus - Its Syntax and Semantics","author":"H. Barendregt","year":"1984","unstructured":"Barendregt, H.: The \u03bb-Calculus - Its Syntax and Semantics. North-Holland, Amsterdam (1984)"},{"key":"7_CR5","unstructured":"Benzm\u00fcller, C., Brown, C.E., Kohlhase, M.: Semantic Techniques for Higher-Order Cut-Elimination. SEKI Tech. Report SR-2004-07, Saarland University (2004)"},{"key":"7_CR6","unstructured":"Br\u00fcnnler, K.: Deep Inference and Symmetry in Classical Proofs. Logos (2004)"},{"key":"7_CR7","unstructured":"Bundy, A.: The use of explicit plans to guide inductive proofs. DAI Research Report 349, Department of Artificial Intelligence, University of Edinburgh (1987)"},{"key":"7_CR8","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Rapport de Recherche 3400, INRIA (April 1998)"},{"key":"7_CR9","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1305\/ndjfl\/1093894722","volume":"XIII","author":"M. Fitting","year":"1972","unstructured":"Fitting, M.: Tableau methods of proof for modal logics. Notre Dame Journal of Formal Logic, XIII, 237\u2013247 (1972)","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"7_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-540-45085-6_31","volume-title":"Automated Deduction \u2013 CADE-19","author":"H. Ganzinger","year":"2003","unstructured":"Ganzinger, H., Stuber, J.: Superposition with equivalence reasoning and delayed clause normal form transformation. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 335\u2013349. Springer, Heidelberg (2003)"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF \u2013 A mechanised logic of computation","author":"M.J. Gordon","year":"1979","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF \u2013 A mechanised logic of computation. LNCS, vol.\u00a078. Springer, Heidelberg (1979)"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the theory of types. The Journal of Symbolic Logic\u00a015, 81\u201391 (1950)","journal-title":"The Journal of Symbolic Logic"},{"key":"7_CR13","unstructured":"Huang, X.: Human Oriented Proof Presentation: A Reconstructive Approach. In: Augustin, S. (ed.) DISKI. Infix, Germany, vol.\u00a0112 (1996)"},{"issue":"2","key":"7_CR14","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1145\/23005.23716","volume":"34","author":"N.V. Murray","year":"1987","unstructured":"Murray, N.V., Rosenthal, E.: Inference with path resolution and semantic graphs. Journal of the Association of Computing Machinery\u00a034(2), 225\u2013254 (1987)","journal-title":"Journal of the Association of Computing Machinery"},{"key":"7_CR15","unstructured":"Pfenning, F.: Proof Transformation in Higher-Order Logic. Phd thesis, Carnegie Mellon University (1987)"},{"key":"7_CR16","volume-title":"Die Grundlehren der mathematischen Wissenschaften","author":"K. Sch\u00fctte","year":"1977","unstructured":"Sch\u00fctte, K.: Proof Theory (Originaltitel: Beweistheorie). In: Die Grundlehren der mathematischen Wissenschaften, vol.\u00a0255, Springer, Heidelberg (1977)"},{"key":"7_CR17","volume-title":"Ergebnisse der Mathematik","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First-Order Logic. In: Ergebnisse der Mathematik, vol.\u00a043, Springer, Berlin (1968)"},{"key":"7_CR18","series-title":"series in AI","volume-title":"Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics","author":"L. Wallen","year":"1990","unstructured":"Wallen, L.: Automated proof search in non-classical logics: efficient matrix proof methods for modal and intuitionistic logics. series in AI. MIT Press, Cambridge (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:09:17Z","timestamp":1605643757000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/11532231_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}