{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:09:58Z","timestamp":1725491398975},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540744634"},{"type":"electronic","value":"9783540744641"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74464-1_3","type":"book-chapter","created":{"date-parts":[[2007,9,12]],"date-time":"2007-09-12T06:58:12Z","timestamp":1189580292000},"page":"33-47","source":"Crossref","is-referenced-by-count":3,"title":["On Constructive Cut Admissibility in Deduction Modulo"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bonichon","sequence":"first","affiliation":[]},{"given":"Olivier","family":"Hermant","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","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":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BFb0049326","volume-title":"Computer Science Logic","author":"C. Coquand","year":"1994","unstructured":"Coquand, C.: From semantic to rules: a machine assisted analysis. In: Meinke, K., B\u00f6rger, E., Gurevich, Y. (eds.) CSL 1993. LNCS, vol.\u00a0832, pp. 91\u2013105. Springer, Heidelberg (1994)"},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1093\/logcom\/exi055","volume":"15","author":"M. Marco De","year":"2005","unstructured":"De Marco, M., Lipton, J.: Completeness and cut elimination in Church\u2019s intuitionistic theory of types. Journal of Logic and Computation\u00a015, 821\u2013854 (2005)","journal-title":"Journal of Logic and Computation"},{"key":"3_CR4","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\u00a031, 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"3_CR5","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","volume":"68","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Werner, B.: Proof normalization modulo. The Journal of Symbolic Logic\u00a068(4), 1289\u20131316 (2003)","journal-title":"The Journal of Symbolic Logic"},{"key":"3_CR6","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-1-4613-0897-3_7","volume-title":"Mathematical Logic and Its Applications","author":"A.G. Dragalin","year":"1987","unstructured":"Dragalin, A.G.: A completeness theorem for higher-order intuitionistic logic: an intuitionistic proof. In: Skordev, D.G. (ed.) Mathematical Logic and Its Applications, pp. 107\u2013124. Plenum, New York (1987)"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Dragalin, A.G.: Mathematical Intuitionism: Introduction to Proof Theory. Translation of Mathematical Monographs. American Mathematical Society vol. 67 (1988)","DOI":"10.1090\/mmono\/067"},{"key":"3_CR8","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198505242.001.0001","volume-title":"Elements of Intuitionism","author":"M. Dummett","year":"2000","unstructured":"Dummett, M.: Elements of Intuitionism. Oxford University Press, Oxford (2000)"},{"key":"3_CR9","unstructured":"Hermant, O.: M\u00e9thodes S\u00e9mantiques en D\u00e9duction Modulo. PhD thesis, Universit\u00e9 Paris 7 - Denis Diderot (2005)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1007\/11417170_17","volume-title":"Typed Lambda Calculi and Applications","author":"O. Hermant","year":"2005","unstructured":"Hermant, O.: Semantic cut elimination in the intuitionistic sequent calculus. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 221\u2013233. Springer, Heidelberg (2005)"},{"key":"3_CR11","doi-asserted-by":"publisher","first-page":"405","DOI":"10.2307\/421172","volume":"2","author":"J.-L. Krivine","year":"1996","unstructured":"Krivine, J.-L.: Une preuve formelle et intuitionniste du th\u00e9or\u00e8me de compl\u00e9tude de la logique classique. The Bulletin of Symbolic Logic\u00a02, 405\u2013421 (1996)","journal-title":"The Bulletin of Symbolic Logic"},{"key":"3_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0211-7","volume-title":"Logic for Applications","author":"A. Nerode","year":"1993","unstructured":"Nerode, A., Shore, R.A.: Logic for Applications. Springer, Heidelberg (1993)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1007\/3-540-55602-8_189","volume-title":"Automated Deduction - CADE-11","author":"N. Shankar","year":"1992","unstructured":"Shankar, N.: Proof search in the intuitionistic sequent calculus. In: Kapur, D. (ed.) Automated Deduction - CADE-11. LNCS, vol.\u00a0607, pp. 522\u2013536. Springer, Heidelberg (1992)"},{"key":"3_CR14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First Order Logic","author":"R. Smullyan","year":"1968","unstructured":"Smullyan, R.: First Order Logic. Springer, Heidelberg (1968)"},{"key":"3_CR15","unstructured":"Takeuti, G.: Proof Theory. Studies in Logic and The Foundations of Mathematics, 2nd edn., vol.\u00a081, North-Holland, Amsterdam (1987)"},{"key":"3_CR16","series-title":"Studies in Logic and The Foundations of Mathematics","volume-title":"Constructivism in Mathematics","author":"A.S. Troelstra","year":"1988","unstructured":"Troelstra, A.S., Van Dalen, D.: Constructivism in Mathematics. Studies in Logic and The Foundations of Mathematics, vol.\u00a02. North Holland, Amsterdam (1988)"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.2307\/2272955","volume":"41","author":"W. Veldman","year":"1976","unstructured":"Veldman, W.: An intuitionistic completeness theorem for intuitionistic predicate logic. Journal of Symbolic Logic\u00a041, 159\u2013166 (1976)","journal-title":"Journal of Symbolic Logic"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1007\/3-540-61208-4_20","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"A. Voronkov","year":"1996","unstructured":"Voronkov, A.: Proof-search in intuitionistic logic based on constraint satisfaction. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS, vol.\u00a01071, pp. 312\u2013329. Springer, Heidelberg (1996)"},{"key":"3_CR19","volume-title":"Handbook of Automated Reasoning","author":"A. Waaler","year":"2001","unstructured":"Waaler, A.: Connection in Nonclassical Logics. In: Handbook of Automated Reasoning, vol.\u00a0II, North Holland, Amsterdam (2001)"},{"key":"3_CR20","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/978-94-017-1754-0_5","volume-title":"Handbook of Tableau Methods","author":"A. Waaler","year":"1999","unstructured":"Waaler, A., Wallen, L.: Tableaux for Intutionistic Logics. In: Handbook of Tableau Methods, pp. 255\u2013296. Kluwer Academic Publishers, Boston (1999)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74464-1_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T21:36:45Z","timestamp":1708205805000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74464-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540744634","9783540744641"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74464-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}