{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:57:46Z","timestamp":1725487066658},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540335207"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-33521-8_15","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T03:10:01Z","timestamp":1183432201000},"page":"153-162","source":"Crossref","is-referenced-by-count":3,"title":["Tableau Method with Free Variables for Intuitionistic Logic"],"prefix":"10.1007","author":[{"given":"Boris","family":"Konev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Lyaletski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0747-7171(03)00026-9","volume":"36","author":"B. Beckert","year":"2003","unstructured":"1. B. Beckert. Depth-.rst proof search without backtracking for free-variable clausal tableaux. Journal of Symbolic Computation, 36:117\u2013138, 2003.","journal-title":"Journal of Symbolic Computation"},{"key":"15_CR2","unstructured":"2. K. Broda. The relationship between semantic tableau and resolution theorem proving. In Proc. of Workshop on Logic, Debrecen, Hungary, 1980."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"3. D. Gabbay. Labelled deductive systems. Oxford university press, 1996.","DOI":"10.1093\/oso\/9780198538332.001.0001"},{"key":"15_CR4","first-page":"545","volume":"2083","author":"M. Giese","year":"2001","unstructured":"4. M. Giese. Incremental closure of free variable tableaux. In Proc. IJCAR'01, vol. 2083 of LNCS, pp. 545\u2013560, 2001.","journal-title":"Proc. IJCAR'01 LNCS"},{"key":"15_CR5","doi-asserted-by":"crossref","unstructured":"5. R. H\u00e4hnle. Tableaux and related methods. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, vol. I, chapter 3, pp. 101\u2013178. Elsevier, 2001.","DOI":"10.1016\/B978-044450813-3\/50005-9"},{"key":"15_CR6","first-page":"94","volume":"293","author":"B. Konev","year":"2002","unstructured":"6. B. Konev and T. Jebelean. Solution lifting method for handling metavariables in the THEOREMA system. Zapiski Nauchnykh Seminarov POMI, 293:94\u2013117, 2002. English translation: Journal of Mathematical Sciences, Springer\/Kluwer\/Plenum, to appear.","journal-title":"Zapiski Nauchnykh Seminarov POMI"},{"issue":"3","key":"15_CR7","first-page":"88","volume":"5","author":"C. Kreitz","year":"1999","unstructured":"7. C. Kreitz and J. Otten. Connection-based theorem proving in classical and non-classical logics. J. UCS, 5(3):88\u2013112, 1999.","journal-title":"J. UCS"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"8. A. Lyaletski, K. Vershinin, A. Degtyarev, and A. Paskevich. System for automated deduction (SAD): Linguistic and deductive peculiarities. In Proc. of Intelligent Information Systems 2002, Advances in Soft Computing, pp. 413\u2013 422. Physica\/Springer Verlag, 2002.","DOI":"10.1007\/978-3-7908-1777-5_44"},{"key":"15_CR9","unstructured":"9. A. V. Lyaletski. Gentzen calculi and admissible substitutions. In Actes Preliminaieres, du Symposium Franco-Sovietique \u201cInformatika-91\u201d, pp. 99\u2013111, Grenoble, France, 1991."},{"key":"15_CR10","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1007\/978-3-642-85983-0_11","volume-title":"Constraint Programming","author":"G. Mints","year":"1994","unstructured":"10. G. Mints. Resolution strategies for the intuitionistic logic. In Constraint Programming, pp. 289\u2013311. Springer, Berlin, Heidelberg, 1994."},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"11. J. Otten. ileanTAP: An intuitionistic theorem prover. In Proc. TABLEAUX'97, vol. 1227 of LNCS, pp. 307\u2013312, 1997.","DOI":"10.1007\/BFb0027422"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"12. J. Otten and C. Kreitz. A connection based proof method for intuitionistic logic. In Proc. TABLEAUX'95, vol. 918 of LNCS, pp. 122\u2013137, 1995.","DOI":"10.1007\/3-540-59338-1_32"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"13. J. Otten and C. Kreitz. A uniform proof procedure for classical and nonclassical logics. In KI-96, vol. 1137 of LNCS, pp. 307\u2013319, 1996.","DOI":"10.1007\/3-540-61708-6_70"},{"key":"15_CR14","unstructured":"14. S. Reeves. Semantic tableaux as framework for automated theorem-proving. In C. S. Mellish and J. Hallam, editors, Proc. AISB-87, pp. 125\u2013139, 1987."},{"key":"15_CR15","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"15. J. A. Robinson. A machine oriented logic based on the resolution principle. J. Assoc. Comput. Mach, 12:23\u201341, 1965.","journal-title":"J. Assoc. Comput. Mach"},{"key":"15_CR16","doi-asserted-by":"crossref","unstructured":"16. S. Schmitt and C. Kreitz. Deleting redundancy in proof reconstruction. In Proc. TABLEAUX'98, vol. 1397 of LNCS, pp. 262\u2013276, 1998.","DOI":"10.1007\/3-540-69778-0_27"},{"key":"15_CR17","doi-asserted-by":"crossref","unstructured":"17. A. Shankar. Proof search in the intuitionistic sequent calculus. In Proc. CADE'92, vol. 607 of LNCS, pp. 522\u2013536, 1992.","DOI":"10.1007\/3-540-55602-8_189"},{"key":"15_CR18","doi-asserted-by":"crossref","unstructured":"18. T. Tammet. A resolution theorem prover for intuitionistic logic. In Proc. CADE-13, vol. 1104 of LNCS, pp. 2\u201316, 1996.","DOI":"10.1007\/3-540-61511-3_65"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"19. A. Voronkov. Proof search in intuitionistic logic based on constraint satisfaction. In Proc. TABLEAUX'96, vol. 1071 of LNCS, pp. 312\u2013329, 1996.","DOI":"10.1007\/3-540-61208-4_20"},{"key":"15_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":"20. A. Waaler and L. Wallen. Tableaux for intuitionistic logics. In M. D'Agostino, D. Gabbay, R. H\u00e4hnle, and J. Posegga, editors, Handbook of Tableau Methods, pp. 255\u2013296. Kluwer, Dordrecht, 1999."},{"key":"15_CR21","volume-title":"Automated Deduction in Nonclassical Logics","author":"L. Wallen","year":"1990","unstructured":"21. L. Wallen. Automated Deduction in Nonclassical Logics. MIT Press: Cambridge, 1990."}],"container-title":["Advances in Soft Computing","Intelligent Information Processing and Web Mining"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-33521-8_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,15]],"date-time":"2024-02-15T18:00:07Z","timestamp":1708020007000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-33521-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540335207"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-33521-8_15","relation":{},"subject":[]}}