{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:09:24Z","timestamp":1725664164977},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540612087"},{"type":"electronic","value":"9783540683681"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61208-4_19","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:19:15Z","timestamp":1330291155000},"page":"295-311","source":"Crossref","is-referenced-by-count":4,"title":["On the intuitionistic force of classical search (Extended abstract)"],"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,1]]},"reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"H. Barendregt. Lambda calculi with types. In: S. Abramsky, Dov M. Gabbay and T. S. E. Maibaum (editors), Handbook of Logic in Computer Science, Volume 2, 117\u2013310, Oxford Science Publications, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"19_CR2","unstructured":"M. Dummett. Elements of Intuitionism. Oxford University Press, 1980."},{"key":"19_CR3","unstructured":"M.C. Fitting. Resolution for intuitionistic logic. In Z. W. Ras and M. Zemankova (editors), Methodologies for intelligent systems, 400\u2013407, Elsevier, 1987."},{"key":"19_CR4","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF00244394","volume":"4","author":"M.C. Fitting","year":"1988","unstructured":"M.C. Fitting. First-order modal tableaux. Journal of Automated Reasoning, 4:191\u2013214, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR5","first-page":"405","volume":"176\u2013210","author":"G. Gentzen","year":"1934","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schliessen. Mathematische Zeitschrift, 176\u2013210, 405\u2013431, 1934.","journal-title":"Mathematische Zeitschrift"},{"key":"19_CR6","unstructured":"J. Herbrand. Investigations in proof theory. In: J. van Heijenoort (editor), From Prege to G\u00f6del, Harvard University Press, 1967."},{"key":"19_CR7","volume-title":"Lecture Notes in Computer Science 933","author":"H. Herbelin","year":"1995","unstructured":"H. Herbelin. A \u03bb-calculus structure isomorphic to sequent calculus structure. In: Proc. Computer Science Logic '94, Kazimierz, Poland, Lecture Notes in Computer Science 933, Springer, 1995."},{"issue":"2","key":"19_CR8","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00881956","volume":"13","author":"R. H\u00e4hnle","year":"1994","unstructured":"R. H\u00e4hnle and P.H. Schmitt. The liberalized \u03b4-rule in free variable semantic tableaux. Journal of Automated Reasoning, 13(2):211\u2013222, 1994.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR9","first-page":"1","volume":"10","author":"S.C. Kleene","year":"1952","unstructured":"S.C. Kleene. Permutability of inferences in Gentzen's calculi LK and LJ. Mem. Amer. Math. Soc., 10:1\u201326, 1952.","journal-title":"Mem. Amer. Math. Soc."},{"key":"19_CR10","unstructured":"J.W. Klop. Term Rewriting Systems. In: S. Abramsky, Dov M. Gabbay and T. S. E. Maibaum (editors), Handbook of Logic in Computer Science, Volume 2,1\u2013116, Oxford Science Publications, 1992."},{"key":"19_CR11","unstructured":"B. Meltzer. Prolegomena to a theory of efficiency of proof procedures. In: Artificial Intelligence and Heuristic Programming, 15\u201333, Edinburgh University Press, 1971."},{"key":"19_CR12","doi-asserted-by":"crossref","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 App. Logic, 51:125\u2013157, 1991.","journal-title":"Ann. Pure App. Logic"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"H.-J. Ohlbach. A resolution calculus for modal logics. In: E. Lusk and R. Overbeek (editors), Proc. 9th. CADE, Lecture Notes in Computer Science 310, 500\u2013516, Springer, 1988.","DOI":"10.1007\/BFb0012852"},{"key":"19_CR14","unstructured":"M. Parigot. \u03bb\u03bc-calculus: an algorithmic interpretation of classical natural deduction. In: Proc. LPAR 92, St. Petersburg, Lecture Notes in Computer Science 624, 190\u2013201, Springer, 1992."},{"key":"19_CR15","unstructured":"M. Parigot. Church-Rosser property in classical free deduction. In: Logical Environments, G. Huet and G. Plotkin (editors), Cambridge University Press, 1993."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"M. Parigot. Strong normalization for second order classical natural deduction. In: Proc. LICS 93, 39\u201347, IEEE Computer Soc. Press, 1993.","DOI":"10.1109\/LICS.1993.287602"},{"key":"19_CR17","volume-title":"Natural deduction: a proof-theoretical study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz. Natural deduction: a proof-theoretical study. Almqvist & Wiksell, Stockholm, 1965."},{"key":"19_CR18","unstructured":"D.J. Pym. Proofs, Search and Computation in General Logic. Ph.D. thesis, University of Edinburgh, 1990."},{"key":"19_CR19","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1007\/BF01063152","volume":"54","author":"D.J. Pym","year":"1995","unstructured":"D.J. Pym. A note on the proof theory of the s\u03bbII-calculus. Studia Logica, 54:199\u2013230, 1995.","journal-title":"Studia Logica"},{"issue":"2","key":"19_CR20","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1093\/logcom\/4.2.175","volume":"4","author":"D.J. Pym","year":"1994","unstructured":"D.J. Pym and J.A. Harland. A uniform proof-theoretic investigation of linear logic programming. Journal of Logic and Computation, 4(2):175\u2013207, 1994.","journal-title":"Journal of Logic and Computation"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"D.J. Pym and L.A. Wallen. Proof-search in the \u03bbII-calculus. In: G. Huet and G. Plotkin (editors), Logical Frameworks, 309\u2013340, Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.013"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"D.J. Pym and L.A. Wallen. Logic programming via proof-valued computations. In: K. Broda (editor), UK Conference on Logic Programming, 253\u2013262, Springer WICS, 1992.","DOI":"10.1007\/978-1-4471-3421-3_14"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"N. Shankar. Proof search in the intuitionistic sequent calculus. In: D. Kapur (editor), Proc. CADE 11, Lecture Notes in Artificial Intelligence 607, Springer, 1992.","DOI":"10.1007\/3-540-55602-8_189"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"R.M. Smullyan. First-order logic, Ergebnisse der Mathematik 43, Springer, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"19_CR25","series-title":"Proc. AISB 85","first-page":"35","volume-title":"Artificial Intelligence and its Applications","author":"L.A. Wallen","year":"1985","unstructured":"L.A. Wallen. Generating connection calculi from tableau-and sequent-based proof systems. In: A.G. Cohn and J.R. Thomas (editors), Artificial Intelligence and its Applications, 35\u201350, John Wiley & Sons, 1986. Proc. AISB 85, Warwick, England, April 1985."},{"key":"19_CR26","unstructured":"L.A. Wallen. Matrix proof methods for modal logics. In: J. McDermott (editor), Proc. 10th. IJCAI, 917\u2013923, Morgan Kaufmann, 1987."},{"key":"19_CR27","unstructured":"L.A. Wallen. Automated Deduction in Non-Classical Logics. MIT Press, 1990."},{"key":"19_CR28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0003-4843(74)90010-2","volume":"7","author":"J. Zucker","year":"1974","unstructured":"J. Zucker. The correspondence between cut-elimination and normalisation. Ann. Math. Logic 7, 1\u2013112, 1974.","journal-title":"Ann. Math. Logic"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61208-4_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:20:57Z","timestamp":1713633657000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61208-4_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540612087","9783540683681"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-61208-4_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}