{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:00:48Z","timestamp":1725490848557},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_10","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"132-146","source":"Crossref","is-referenced-by-count":3,"title":["A Labelled System for IPL with Variable Splitting"],"prefix":"10.1007","author":[{"given":"Roger","family":"Antonsen","sequence":"first","affiliation":[]},{"given":"Arild","family":"Waaler","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/11554554_5","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Antonsen","year":"2005","unstructured":"Antonsen, R., Waaler, A.: Consistency of variable splitting in free variable systems of first-order logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 33\u201347. Springer, Heidelberg (2005)"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-006-9055-9","volume":"38","author":"R. Antonsen","year":"2007","unstructured":"Antonsen, R., Waaler, A.: Liberalized variable splitting. Journal of Automated Reasoning\u00a038, 3\u201330 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving. 2. edn. Vieweg Verlag (1987)","DOI":"10.1007\/978-3-322-90102-6"},{"key":"10_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. Journal of Symbolic Logic\u00a057, 795\u2013807 (1992)","journal-title":"Journal of Symbolic Logic"},{"key":"10_CR5","unstructured":"Giese, M.: Proof Search without Backtracking for Free Variable Tableaux. PhD thesis, Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe (July 2002)"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"TABLEAUX 2007","author":"C.M. Hansen","year":"2007","unstructured":"Hansen, C.M., Antonsen, R., Waaler, A.: Incremental closure of variable splitting tableaux, position paper. In: Olivetti, N. (ed.) TABLEAUX 2007, Aix en Provence, France. LNCS, vol.\u00a04548, Springer, Heidelberg (2007)"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF01627506","volume":"31","author":"J. Hudelmaier","year":"1992","unstructured":"Hudelmaier, J.: Bounds on cut-elimination in intuitionistic propositional logic. Archive for Mathematical Logic\u00a031, 331\u2013353 (1992)","journal-title":"Archive for Mathematical Logic"},{"issue":"3","key":"10_CR8","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. Journal of Universal Computer Science\u00a05(3), 88\u2013112 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"10_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/11554554_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Otten","year":"2005","unstructured":"Otten, J.: Clausal connection-based theorem proving in intuitionistic first-order logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 245\u2013261. Springer, Heidelberg (2005)"},{"key":"10_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/11554554_28","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"T. Raths","year":"2005","unstructured":"Raths, T., Otten, J., Kreitz, C.: The ILTP library: Benchmarking automated theorem provers for intuitionistic logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 333\u2013337. Springer, Heidelberg (2005)"},{"issue":"5","key":"10_CR11","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1093\/logcom\/2.5.619","volume":"2","author":"D. Sahlin","year":"1992","unstructured":"Sahlin, D., Franz\u00e9n, T., Haridi, S.: An intuitionistic predicate logic theorem prover. Journal of Logic and Computation\u00a02(5), 619\u2013656 (1992)","journal-title":"Journal of Logic and Computation"},{"key":"10_CR12","volume-title":"Ergebnisse der Mathematik und ihrer Grenzgebiete","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan, R.M.: First-Order Logic. In: Ergebnisse der Mathematik und ihrer Grenzgebiete, vol.\u00a043, Springer, New York (1968)"},{"key":"10_CR13","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"A.S. Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000)","edition":"2"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"1487","DOI":"10.1016\/B978-044450813-3\/50024-2","volume-title":"Handbook of Automated Reasoning, ch. 22","author":"A. Waaler","year":"2001","unstructured":"Waaler, A.: Connections in nonclassical logics. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, ch. 22, vol.\u00a0II, pp. 1487\u20131578. Elsevier, Amsterdam (2001)"},{"key":"10_CR15","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/978-94-017-1754-0_5","volume-title":"Handbook of Tableaux Methods","author":"A. Waaler","year":"1999","unstructured":"Waaler, A., Wallen, L.: Tableaux for intuitionistic logics. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableaux Methods, pp. 255\u2013296. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"10_CR16","volume-title":"Automated deduction in nonclassical logics","author":"L.A. Wallen","year":"1990","unstructured":"Wallen, L.A.: Automated deduction in nonclassical logics. MIT Press, Cambridge (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:00Z","timestamp":1619517180000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}