{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:20:58Z","timestamp":1725664858126},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540616979"},{"type":"electronic","value":"9783540706359"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61697-7_1","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:12:38Z","timestamp":1330294358000},"page":"1-21","source":"Crossref","is-referenced-by-count":1,"title":["Problem-oriented applications of automated theorem proving"],"prefix":"10.1007","author":[{"given":"W.","family":"Bibel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Korn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Kreitz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Schmitt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"P. Andrews. Transforming matings into natural deduction proofs. In CADE-5, LNCS 87, pp. 281\u2013292. Springer, 1980.","DOI":"10.1007\/3-540-10009-1_22"},{"key":"1_CR2","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1007\/BF00243811","volume":"7","author":"P. Andrews","year":"1991","unstructured":"P. Andrews. More on the problem of finding a mapping between clause representation and natural-deduction representation. Journal of Automated Reasoning, Vol. 7, pp 285\u2013286, 1991.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"1_CR3","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1145\/2363.2528","volume":"7","author":"J. L. Bates","year":"1985","unstructured":"J. L. Bates, R. L. Constable. Proofs as programs. ACM Transactions on Programming Languages and Systems, 7(1):113\u2013136, January 1985.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR4","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg Verlag, 21987."},{"key":"1_CR5","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":"1_CR6","doi-asserted-by":"crossref","unstructured":"D. Brand Proving theorems with the modification method. In J. Hopcroft e. a., eds. SIAM Journal of Computing Vol. 4, pp. 412\u2013430. Philadelphia, 1975.","DOI":"10.1137\/0204036"},{"key":"1_CR7","unstructured":"R. L. Constable et. al. Implementing Mathematics with the NuPRL proof development system. Prentice Hall, 1986."},{"key":"1_CR8","volume-title":"Preprint 94-10","author":"B. I. Dahn","year":"1994","unstructured":"B. I. Dahn, J. Gehne, T. Honigmann, L. Walther, A. Wolf. Integrating Logical Functions with ILF, Preprint 94-10, Humboldt University Berlin, 1994."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"U. Egly, T. Rath. On the practical value of different definitional translation to normal form. To appear in CADE-13, Springer, 1996.","DOI":"10.1007\/3-540-61511-3_103"},{"key":"1_CR10","unstructured":"M. C. Fitting. Intuitionistic logic, model theory and forcing. Studies in logic and the foundations of mathematics. North-Holland, 1969."},{"key":"1_CR11","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":"1_CR12","unstructured":"K. Genther. Repr\u00e4sentation von Konnektionsbeweisen in Gentzen-Kalk\u00fclen durch Transformation und Strukturierung. Tech. Rep. AIDA-95-12, TH Darmstadt, 1995."},{"key":"1_CR13","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schlie\u03b2en. Mathematische Zeitschrift, 39:176\u2013210, 405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"1_CR14","volume-title":"Intuitionism \u2014 An Introduction","author":"A. Heyting","year":"1971","unstructured":"A. Heyting. Intuitionism \u2014 An Introduction. North Holland Publishing Company, Amsterdam, 31971."},{"key":"1_CR15","unstructured":"D. Korn. KonSequenz \u2014 ein Konnektionsmethoden-gesteuertes Sequenzenbeweisverfahren. Master-thesis, TH Darmstadt, 1993."},{"key":"1_CR16","unstructured":"D. Korn. Efficiently Deciding Intuitionistic Propositional Logic via Translation into Classical Logic. Tech. Rep. AIDA-96-09, TH Darmstadt, 1996."},{"issue":"1","key":"1_CR17","first-page":"75","volume":"4","author":"C. Kreitz","year":"1996","unstructured":"C. Kreitz. Formal Mathematics for Verifiably Correct Program Synthesis. Journal of the Interest Group in Pure and Applied Logics (IGPL), 4(1):75\u201394, 1996.","journal-title":"Journal of the Interest Group in Pure and Applied Logics (IGPL)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"C. Kreitz, J. Otten, S. Schmitt. Guiding Program Development Systems by a Connection Based Proof Strategy. In M. Proietti, editor, 5th International Workshop on Logic Program Synthesis and Transformation, LNCS 1048, pp. 137\u2013151, Springer Verlag, 1996.","DOI":"10.1007\/3-540-60939-3_10"},{"key":"1_CR19","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S. A. Kripke","year":"1963","unstructured":"S. A. Kripke. Semantical analysis of modal logic I. Normal modal propositional calculi. Zeitschrift f. mathematische Logik u. Grundlagen d. Mathematik 9, pp 67\u201396, 1963.","journal-title":"Zeitschrift f. mathematische Logik u. Grundlagen d. Mathematik"},{"key":"1_CR20","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":"1_CR21","unstructured":"C. Lingenfelder. Structuring computer generated proofs. IJCAI-89, 1989."},{"key":"1_CR22","unstructured":"C. Lingenfelder. Transformation and Structuring of Computer Generated Proofs. PhD thesis, Universit\u00e4t Kaiserslautern, 1990."},{"key":"1_CR23","unstructured":"R. C. Moore. Reasoning about Knowledge and Action IJCAI-77, pp 223\u2013227, Stanford, California 94305, 1977."},{"issue":"no.6","key":"1_CR24","doi-asserted-by":"crossref","first-page":"691","DOI":"10.1093\/logcom\/1.5.691","volume":"1","author":"H. J. Ohlbach","year":"1991","unstructured":"H. J. Ohlbach. Semantics-Based Translation Methods for Modal Logics. Journal of Logic and Computation, Vol. 1, no. 6, pp 691\u2013746, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"1_CR25","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":"1_CR26","doi-asserted-by":"crossref","unstructured":"J. Otten, C. Kreitz. T-string-unification: unifying prefixes in non-classical proof methods. TABLEAUX-96, LNAI 1071, pp. 244\u2013260, Springer, 1996.","DOI":"10.1007\/3-540-61208-4_16"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"J. Otten, C. Kreitz. A Uniform Proof Procedure for Classical and Non-Classical Logics. To appear in KI-96, Springer, 1996.","DOI":"10.1007\/3-540-61708-6_70"},{"key":"1_CR28","unstructured":"F. Pfenning. Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, January 1987."},{"key":"1_CR29","doi-asserted-by":"crossref","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 Journal of ACM, Vol. 12, pp 23\u201341, 1965.","journal-title":"Journal of ACM"},{"key":"1_CR30","unstructured":"G. Robinson and L. Wos., Paramodulation and theorem proving in first order theories with equality. In B. Meltzer and D. Michie, eds., Machine Intelligence 4, pp. 135\u2013150, Edinburgh University Press, 1969."},{"key":"1_CR31","unstructured":"S. Schmitt. Ein erweiterter intuitionistischer Sequenzenkalk\u00fcl und dessen Anwendung im intuitionistischen Konnektionsbeweisen. Tech. Rep. AIDA-95-01, TH Darmstadt, 1995."},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"S. Schmitt, C. Kreitz. On transforming intuitionistic matrix proofs into standard-sequent proofs. TABLEAUX-95, LNAI 918, pp. 106\u2013121, Springer, 1995.","DOI":"10.1007\/3-540-59338-1_31"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"S. Schmitt, C. Kreitz. Converting Non-Classical Matrix Proofs into Sequent-Style Systems. To appear in CADE-13, Springer, 1996.","DOI":"10.1007\/3-540-61511-3_104"},{"key":"1_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-66473-1","volume-title":"Proof theory","author":"K. Sch\u00fctte","year":"1977","unstructured":"K. Sch\u00fctte. Proof theory. Springer-Verlag, New York, 1977."},{"key":"1_CR35","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-94-009-6259-0_4","volume-title":"Handbook of Philosophical Logic, Vol. II","author":"J. Benthem Van","year":"1984","unstructured":"J. Van Benthem. Correspondence Theory. In: D. Gabbay and F. Guenther (eds.): Handbook of Philosophical Logic, Vol. II, pp. 167\u2013247, D. Reidel Publishing Company, Dordrecht, 1984."},{"key":"1_CR36","unstructured":"L. Wallen. Automated deduction in non-classical logics. MIT Press, 1990."},{"key":"1_CR37","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/BF00245820","volume":"6","author":"L. Wos","year":"1990","unstructured":"L. Wos. The problem of finding a mapping between clause representation and natural-deduction representation. Journal of Automated Reasoning, Vol. 6, pp 211\u2013212, 1990.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Design and Implementation of Symbolic Computation Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61697-7_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:09:22Z","timestamp":1605647362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61697-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616979","9783540706359"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/3-540-61697-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}