{"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":1761611300880},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615118"},{"type":"electronic","value":"9783540686873"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61511-3_104","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:50:44Z","timestamp":1330293044000},"page":"418-432","source":"Crossref","is-referenced-by-count":14,"title":["Converting non-classical matrix proofs into sequent-style systems"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Schmitt","sequence":"first","affiliation":[]},{"given":"Christoph","family":"Kreitz","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,4]]},"reference":[{"key":"41_CR1","unstructured":"E. W. Beth. The foundations of mathematics. North-Holland, 1959."},{"key":"41_CR2","doi-asserted-by":"crossref","unstructured":"W. Bibel, S. Br\u00fcning, U. Egly, T. Rath. Komet. In CADE-12, LNAI 814, pp. 783\u2013787. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_60"},{"key":"41_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. J. of the ACM, 28:633\u2013645, 1981.","journal-title":"J. of the ACM"},{"key":"41_CR4","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"41_CR5","unstructured":"B. I. Dahn, J. Gehne, Th. Honigmann, L. Walther, A. Wolf. Integrating Logical Functions with ILF; Preprint 94-10, Humboldt University Berlin, 1994."},{"key":"41_CR6","unstructured":"M. C. Fitting. Intuitionistic logic, model theory and forcing. Studies in logic and the foundations of mathematics. North-Holland, 1969."},{"key":"41_CR7","doi-asserted-by":"crossref","unstructured":"M. C. Fitting. Proof Methods for Modal and Intuitionistic Logic. D. Reidel, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"41_CR8","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, W. Bibel. Setheo: A high-performance theorem prover. Journal of Automated Reasoning, 8:183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"41_CR9","unstructured":"C. Lingenfelder. Structuring computer generated proofs. IJCAI-89, 1989."},{"key":"41_CR10","unstructured":"C. Lingenfelder. Transformation and Structuring of Computer Generated Proofs. PhD thesis, Universit\u00e4t Kaiserslautern, 1990."},{"key":"41_CR11","unstructured":"H. J. Ohlbach. A resolution calculus for modal logics. Ph.D. Thesis, Universit\u00e4t Kaiserslautern, 1988."},{"key":"41_CR12","doi-asserted-by":"crossref","unstructured":"J. Otten, C. Kreitz. A connection based proof method for intuitionistic logic. TABLEAUX-95, LNAI 918, pp. 122\u2013137, Springer, 1995.","DOI":"10.1007\/3-540-59338-1_32"},{"key":"41_CR13","doi-asserted-by":"crossref","unstructured":"J. Otten, C. Kreitz. A Uniform Proof Procedure for Classical and Non-Classical Logics Technical Report, TH Darmstadt, 1996.","DOI":"10.1007\/3-540-61708-6_70"},{"issue":"1","key":"41_CR14","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. J. of the ACM, 12(1):23\u201341, 1965.","journal-title":"J. of the ACM"},{"key":"41_CR15","doi-asserted-by":"crossref","unstructured":"S. Schmitt, C. Kreitz. On transforming intuitionistic matrix proofs into standardsequent proofs. TABLEAUX-95, LNAI 918, pp. 106\u2013121, Springer, 1995.","DOI":"10.1007\/3-540-59338-1_31"},{"key":"41_CR16","unstructured":"S. Schmitt. Ein erweiterter intuitionistischer Sequenzenkalk\u00fcl und dessen Anwendung im intuitionistischen Konnektionsbeweisen. TH Darmstadt, 1994."},{"key":"41_CR17","unstructured":"L. Wallen. Matrix proof methods for modal logics. IJCAI-87, p. 917\u2013923. 1987."},{"key":"41_CR18","unstructured":"L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990."},{"key":"41_CR19","doi-asserted-by":"crossref","unstructured":"L. Wos Et. Al. Automated reasoning contributes to mathematics and logic. CADE-10, LNCS 449, p. 485\u2013499. Springer 1990.","DOI":"10.1007\/3-540-52885-7_109"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 Cade-13"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61511-3_104.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:12Z","timestamp":1605647232000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61511-3_104"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615118","9783540686873"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61511-3_104","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}