{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:20Z","timestamp":1761611300210},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_66","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:50:27Z","timestamp":1330293027000},"page":"17-31","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Proof-terms for classical and intuitionistic resolution"],"prefix":"10.1007","author":[{"given":"Eike","family":"Ritter","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pym","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lincoln","family":"Wallen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"3_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"P.B. Andrews. Theorem-proving with general matings. JACM, 28:193\u2013214, 1981.","journal-title":"JACM"},{"issue":"2","key":"3_CR2","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BF00881838","volume":"10","author":"A. Avron","year":"1993","unstructured":"A. Avron. Gentzen-type systems, resolution and tableaux. J. Automat. Reas., 10(2):265\u2013282, 1993.","journal-title":"J. Automat. Reas."},{"key":"3_CR3","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel. On matrices with connections. JACM, 28:633\u2013645, 1981.","journal-title":"JACM"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"W. Bibel. Computationally improved versions of Herbrand's theorem. In: Stern (ed.), Proc. of the Herbrand Colloquium, North-Holland, 1982.","DOI":"10.1016\/S0049-237X(08)71874-3"},{"key":"3_CR5","unstructured":"M. Dummett. Elements of Intuitionism. Oxford University Press, 1980."},{"key":"3_CR6","unstructured":"M.C. Fitting. Resolution for intuitionistic logic. In: Z. W. Ras and M. Zemankova (eds.), Methodologies for intelligent systems, 400\u2013407, Elsevier, 1987."},{"key":"3_CR7","first-page":"191","volume":"4","author":"M.C. Fitting","year":"1988","unstructured":"M.C. Fitting. First-order modal tableaux. J. Automat. Reas., 4:191\u2013214, 1988.","journal-title":"J. Automat. Reas."},{"key":"3_CR8","first-page":"405","volume":"176\u2013210","author":"G. Gentzen","year":"1934","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schliessen. Math. Zeit., 176\u2013210, 405\u2013431, 1934.","journal-title":"Math. Zeit."},{"key":"3_CR9","unstructured":"S.Yu Maslov. Theory of Deductive Systems and its Applications. MIT Press, 1987."},{"key":"3_CR10","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"D. Miller, G. Nadathur, A. \u0160\u010dedrov and F. Pfenning. Uniform proofs as a foundation for logic programming. Ann. Pure Appl. Logic, 51:125\u2013157, 1991.","journal-title":"Ann. Pure Appl. Logic"},{"key":"3_CR11","unstructured":"G. Mints. Gentzen-type systems and resolution rules part I: Propositional logic. In: P. Martin-L\u00f6f and G. Mints (eds.), Proc. COLOG-88, LNCS 417, 198\u2013231, 1990."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"H.J. Ohlbach. A resolution calculus for modal logics. In: E. Lusk and R. Overbeek (eds.), Proc. 9th CADE, LNCS 310, 500\u2013516, 1988.","DOI":"10.1007\/BFb0012852"},{"key":"3_CR13","first-page":"190","volume":"624","author":"M. Parigot","year":"1992","unstructured":"M. Parigot. \u03bb\u03bc-calculus: an algorithmic interpretation of classical natural deduction. In: Proc. LPAR '98, LNCS 624, 190\u2013201, 1992.","journal-title":"LNCS"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"D. Pym and L. Wallen. Proof-search in the \u03bb\u03c0-calculus. In: G. Huet and G. Plotkin (eds.), Logical Frameworks, 309\u2013340, Cambridge Univ. Press, 1991.","DOI":"10.1017\/CBO9780511569807.013"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"D. Pym and L. Wallen. Logic programming via proof-valued computations. In: K. Broda (ed.), ALPUK '92, 253\u2013262, WICS, Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4471-3421-3_14"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"E. Ritter, D. Pym and L. Wallen. On the intuitionistic force of classical search. In: P. Miglioli, U. Moscato, D. Mundici and M. Ornaghi (eds.), Proc. Tableaux '96, LNCS 1071, 295\u2013311, 1996.","DOI":"10.1007\/3-540-61208-4_19"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"J. Robinson. A machine-oriented logic based on the resolution principle. JACM, 12:23\u201341, 1965.","journal-title":"JACM"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"R. Smullyan. First-order logic. Ergebnisse der Math. 43, Springer-Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7_4"},{"key":"3_CR19","unstructured":"L. Wallen. Generating connection calculi from tableau-and sequent-based proof systems. In: A.G. Cohn and J.R. Thomas (eds.), Artificial Intelligence and its Applications, 35\u201350, John Wiley & Sons, 1986, (Proc. AISB'85, 1985)."},{"key":"3_CR20","unstructured":"L. Wallen. Matrix proof methods for modal logics. In: J. McDermott (ed.), Proc. 10th IJCAI, 917\u2013923, Morgan Kaufmann Inc., 1987."},{"key":"3_CR21","unstructured":"L. Wallen. Automated Deduction in Non-Classical Logics. MIT Press, 1990."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_66","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T02:12:43Z","timestamp":1578535963000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_66"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_66","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"4 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}