{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:26:15Z","timestamp":1725470775267},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540396253"},{"type":"electronic","value":"9783540396277"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11853886_25","type":"book-chapter","created":{"date-parts":[[2006,9,13]],"date-time":"2006-09-13T16:40:30Z","timestamp":1158165630000},"page":"293-305","source":"Crossref","is-referenced-by-count":3,"title":["On Herbrand\u2019s Theorem for Intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Lyaletski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Boris","family":"Konev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"Baaz, M., Iemhoff, R.: On the skolemization of existential quantifiers in intuitionistic logic. Annals of Pure and Applied Logic (to appear, 2006)","DOI":"10.1016\/j.apal.2006.02.001"},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving, 2nd edn., Vieweg, Braunschweig (1987)","DOI":"10.1007\/978-3-322-90102-6"},{"issue":"2","key":"25_CR3","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1305\/ndjfl\/1093887533","volume":"17","author":"K.A. Bowen","year":"1976","unstructured":"Bowen, K.A.: An Herbrand theorem for prenex formulas of LJ. Notre Dame Journal of Formal Logic\u00a017(2), 263\u2013266 (1976)","journal-title":"Notre Dame Journal of Formal Logic"},{"issue":"3","key":"25_CR4","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","volume":"57","author":"R. Dyckhoff","year":"1992","unstructured":"Dyckhoff, R.: Contraction-free sequent calculi for intuitionistic logic. J. Symb. Log.\u00a057(3), 795\u2013807 (1992)","journal-title":"J. Symb. Log."},{"issue":"1-2","key":"25_CR5","doi-asserted-by":"crossref","first-page":"101","DOI":"10.3233\/FI-1996-281206","volume":"28","author":"M. Fitting","year":"1996","unstructured":"Fitting, M.: A modal herbrand theorem. Fundam. Inform.\u00a028(1-2), 101\u2013122 (1996)","journal-title":"Fundam. Inform."},{"key":"25_CR6","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled deductive systems","author":"D. Gabbay","year":"1996","unstructured":"Gabbay, D.: Labelled deductive systems. Oxford University Press, Oxford (1996)"},{"issue":"176-210","key":"25_CR7","first-page":"405","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift\u00a039(176-210), 405\u2013433 (1934)","journal-title":"Mathematische Zeitschrift"},{"key":"25_CR8","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/B978-044450813-3\/50005-9","volume-title":"Handbook of Automated Reasoning, ch. 3","author":"R. H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and related methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 3, vol.\u00a0I, pp. 101\u2013178. Elsevier, Amsterdam (2001)"},{"key":"25_CR9","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration (thesis). In: Goldfarb, W. (ed.) Logical writings, Cambridge (1977)"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Konev, B., Lyaletski, A.: Tableau method with free variables for intuitionistic logic. In: Proceedings of the International IIS: IIPWM 2006 Conference. Advances in Soft Computing (to appear, 2006)","DOI":"10.1007\/3-540-33521-8_15"},{"issue":"3","key":"25_CR11","first-page":"88","volume":"5","author":"C. Kreitz","year":"1999","unstructured":"Kreitz, C., Otten, J.: Connection-based theorem proving in classical and non-classical logics. J. UCS\u00a05(3), 88\u2013112 (1999)","journal-title":"J. UCS"},{"key":"25_CR12","doi-asserted-by":"crossref","unstructured":"Lyaletski, A.: Sequent forms of Herbrand theorem and their applications. Annals of Mathematics and Artificial Intelligence (in press)","DOI":"10.1007\/s10472-005-9017-7"},{"key":"25_CR13","unstructured":"Lyaletski, A.V.: Gentzen calculi and admissible substitutions. In: Actes Pr\u00e9liminaieres du Symposium Franco-Sovietique \u201cInformatika-91\u201d, Grenoble, France, pp. 99\u2013111 (1991)"},{"key":"25_CR14","first-page":"48","volume-title":"Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970","author":"S.Y. Maslov","year":"1983","unstructured":"Maslov, S.Y.: An inverse method for establishing deducibility of nonprenex formulas of the predicate calculus. In: Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning 2: Classical Papers on Computational Logic 1967-1970, pp. 48\u201354. Springer, Heidelberg (1983)"},{"key":"25_CR15","unstructured":"Mints, G.: Herbrand theorem. In: Mathematical Theory of Logical Inference, Nauka, Moscow, pp. 311\u2013350 (1967)"},{"key":"25_CR16","unstructured":"Mints, G.: The Skolem method in intuitionistic calculi. In: Proc. Steklov Inst. Math., vol.\u00a0121, pp. 73\u2013109 (1972)"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0027422","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Otten","year":"1997","unstructured":"Otten, J.: ileanTAP: An intuitionistic theorem prover. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS, vol.\u00a01227, pp. 307\u2013312. Springer, Heidelberg (1997)"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/3-540-59338-1_32","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J. Otten","year":"1995","unstructured":"Otten, J., Kreitz, C.: A connection based proof method for intuitionistic logic. In: Baumgartner, P., Posegga, J., H\u00e4hnle, R. (eds.) TABLEAUX 1995. LNCS, vol.\u00a0918, pp. 122\u2013137. Springer, Heidelberg (1995)"},{"key":"25_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/3-540-61708-6_70","volume-title":"KI-96: Advances in Artificial Intelligence","author":"J. Otten","year":"1996","unstructured":"Otten, J., Kreitz, C.: A uniform proof procedure for classical and non-classical logics. In: G\u00f6rz, G., H\u00f6lldobler, S. (eds.) KI 1996. LNCS, vol.\u00a01137, pp. 307\u2013319. Springer, Heidelberg (1996)"},{"key":"25_CR20","unstructured":"Reeves, S.: Semantic tableaux as framework for automated theorem-proving. In: Mellish, C.S., Hallam, J. (eds.) Proc. AISB 1987, pp. 125\u2013139 (1987)"},{"key":"25_CR21","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine oriented logic based on the resolution principle. J. Assoc. Comput. Mach\u00a012, 23\u201341 (1965)","journal-title":"J. Assoc. Comput. Mach"},{"key":"25_CR22","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.) CADE 1992. LNCS, vol.\u00a0607, pp. 522\u2013536. Springer, Heidelberg (1992)"},{"key":"25_CR23","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":"25_CR24","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 intuitionistic logics. In: D\u2019Agostino, M., Gabbay, D., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 255\u2013296. Kluwer, Dordrecht (1999)"},{"key":"25_CR25","volume-title":"Automated Deduction in Nonclassical Logics","author":"L. Wallen","year":"1990","unstructured":"Wallen, L.: Automated Deduction in Nonclassical Logics. MIT Press, Cambridge (1990)"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11853886_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,6]],"date-time":"2024-02-06T12:25:49Z","timestamp":1707222349000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11853886_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540396253","9783540396277"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/11853886_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}