{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:51:35Z","timestamp":1725475895407},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_24","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T00:43:15Z","timestamp":1167439395000},"page":"294-308","source":"Crossref","is-referenced-by-count":1,"title":["Matrix-Based Inductive Theorem Proving"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Kreitz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Smaill, A., Green, I.: Automatic synthesis of recursive programs: The proof-planning paradigm. In: 12th IEEE International Automated Software Engineering Conference, pp. 2\u20139 (1997)","DOI":"10.1109\/ASE.1997.632818"},{"issue":"2","key":"24_CR2","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D. Basin","year":"1996","unstructured":"Basin, D., Walsh, T.: A calculus for and termination of rippling. Journal of Automated Reasoning\u00a016(2), 147\u2013180 (1996)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"24_CR3","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1145\/2363.2528","volume":"7","author":"J. Bates","year":"1985","unstructured":"Bates, J., Constable, R.: Proofs as programs. ACM Transactions on Programming Languages and Systems\u00a07(1), 113\u2013136 (1985)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"24_CR4","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W.: On matrices with connections. Journal of the Association for Computing Machinery\u00a028, 633\u2013645 (1981)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"24_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF03037438","volume":"4","author":"W. Bibel","year":"1986","unstructured":"Bibel, W.: A deductive solution for plan generation. New Generation Computing\u00a04, 115\u2013132 (1986)","journal-title":"New Generation Computing"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving. Vieweg (1987)","DOI":"10.1007\/978-3-322-90102-6"},{"key":"24_CR7","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-49674-2_1","volume-title":"Logic Program Synthesis and Transformation","author":"W. Bibel","year":"1998","unstructured":"Bibel, W., Korn, D., Kreitz, C., Kurucz, F., Otten, J., Schmitt, S., Stolpmann, G.: A multi-level approach to program synthesis. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS (LNAI), vol.\u00a01463, pp. 1\u201325. Springer, Heidelberg (1998)"},{"key":"24_CR8","unstructured":"Biundo, S.: Automated synthesis of recursive algorithms as a theorem proving tool. In: 8th European Conference on Artificial Intelligence (1988)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/3-540-52885-7_84","volume-title":"10th International Conference on Automated Deduction","author":"A. Bundy","year":"1990","unstructured":"Bundy, A., van Harmelen, F., Smaill, A., et al.: Extensions to the rippling-out tactic for guiding inductive proofs. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 132\u2013146. Springer, Heidelberg (1990)"},{"issue":"2","key":"24_CR10","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0004-3702(93)90079-Q","volume":"62","author":"A. Bundy","year":"1993","unstructured":"Bundy, A., Stevens, A., van Harmelen, F., et al.: Rippling: A heuristic for guiding inductive proofs. Artificial Intelligence\u00a062(2), 185\u2013253 (1993)","journal-title":"Artificial Intelligence"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","first-page":"227","volume-title":"An Introduction to the PL\/CV2 Programming Logic","author":"T. Chan","year":"1982","unstructured":"Chan, T.: A decision procedure for checking PL\/CV arithmetic inferences. In: Constable, R.L., Eichenlaub, C.D., Johnson, S.D. (eds.) An Introduction to the PL\/CV2 Programming Logic. LNCS, vol.\u00a0135, pp. 227\u2013264. Springer, Heidelberg (1982)"},{"key":"24_CR12","volume-title":"Implementing Mathematics with the Nu- PRL proof development system","author":"R. Constable","year":"1986","unstructured":"Constable, R., Allen, S., Bromley, M., et al.: Implementing Mathematics with the Nu- PRL proof development system. Prentice Hall, Englewood Cliffs (1986)"},{"key":"24_CR13","unstructured":"Dowek, G., et al.: The Coq proof assistant user\u2019s guide. Institut National de Recherche en Informatique et en Automatique, Report RR 134 (1991)"},{"key":"24_CR14","unstructured":"Hesketh, J.: Using Middle-Out Reasoning to Guide Inductive Theorem Proving. PhD thesis, Dept. of Artificial Intelligence, University of Edinburgh (1991)"},{"key":"24_CR15","series-title":"LNAI","volume-title":"Automated Deduction - CADE-12","author":"D. Hutter","year":"1994","unstructured":"Hutter, D.: Synthesis of Induction Orderings for Existence Proofs. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814. Springer, Heidelberg (1994)"},{"key":"24_CR16","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"288","DOI":"10.1007\/3-540-61511-3_92","volume-title":"Automated Deduction - Cade-13","author":"D. Hutter","year":"1996","unstructured":"Hutter, D., Sengler, C.: INKA, the next generation. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 288\u2013292. Springer, Heidelberg (1996)"},{"key":"24_CR17","doi-asserted-by":"crossref","unstructured":"Kraan, I., Basin, D., Bundy, A.: Logic program synthesis via proof planning. In: 4th International Workshop on Logic Program Synthesis and Transformation, pp. 1\u201314 (1993)","DOI":"10.1007\/978-1-4471-3560-9_1"},{"key":"24_CR18","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-63104-6_20","volume-title":"Automated Deduction - CADE-14","author":"C. Kreitz","year":"1997","unstructured":"Kreitz, C., Mantel, H., Otten, J., Schmitt, S.: Connection-Based Proof Construction in Linear Logic. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 207\u2013221. Springer, Heidelberg (1997)"},{"key":"24_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-60939-3_10","volume-title":"Logic Program Synthesis and Transformation","author":"C. Kreitz","year":"1996","unstructured":"Kreitz, C., Otten, J., Schmitt, S.: Guiding Program Development Systems by a Connection Based Proof Strategy. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol.\u00a01048, pp. 137\u2013151. Springer, Heidelberg (1996)"},{"issue":"3","key":"24_CR20","first-page":"88","volume":"5","author":"C. Kreitz","year":"1999","unstructured":"Kreitz, C., Otten, J.: Connection-based theorem proving in classical and nonclassical logics. Journal of Universal Computer Science\u00a05(3), 88\u2013112 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"24_CR21","unstructured":"Kurucz, F.: Realisierung verschiedender Induktionsstrategien basierend auf dem Rippling-Kalk\u00fcl. Diplomarbeit, Technische Universit\u00e4t Darmstadt (1997)"},{"key":"24_CR22","series-title":"LNAI","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 (LNAI), vol.\u00a0918, pp. 122\u2013137. Springer, Heidelberg (1995)"},{"key":"24_CR23","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-61208-4_16","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J. Otten","year":"1996","unstructured":"Otten, J., Kreitz, C.: T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol.\u00a01071, pp. 244\u2013260. Springer, Heidelberg (1996)"},{"issue":"1-2","key":"24_CR24","doi-asserted-by":"crossref","first-page":"189","DOI":"10.3233\/FI-1999-391210","volume":"39","author":"B. Pientka","year":"1999","unstructured":"Pientka, B., Kreitz, C.: Automating inductive specification proofs. Fundamenta Informatica\u00a039(1-2), 189\u2013209 (1999)","journal-title":"Fundamenta Informatica"},{"key":"24_CR25","unstructured":"Smaill, A., Green, I.: Automating the synthesis of functional programs. Research paper 777, Dept. of Artificial Intelligence, University of Edinburgh (1995)"},{"key":"24_CR26","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/3-540-59338-1_31","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"S. Schmitt","year":"1995","unstructured":"Schmitt, S., Kreitz, C.: On transforming intuitionistic matrix proofs into standardsequent proofs. In: Baumgartner, P., Posegga, J., H\u00e4hnle, R. (eds.) TABLEAUX 1995. LNCS (LNAI), vol.\u00a0918, pp. 106\u2013121. Springer, Heidelberg (1995)"},{"key":"24_CR27","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/3-540-61511-3_104","volume-title":"Automated Deduction - Cade-13","author":"S. Schmitt","year":"1996","unstructured":"Schmitt, S., Kreitz, C.: Converting non-classical matrix proofs into sequent-style systems. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 418\u2013432. Springer, Heidelberg (1996)"},{"key":"24_CR28","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-61511-3_65","volume-title":"Automated Deduction - Cade-13","author":"T. Tammet","year":"1996","unstructured":"Tammet, T.: A resolution theorem prover for intuitionistic logic. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 2\u201316. Springer, Heidelberg (1996)"},{"key":"24_CR29","volume-title":"Automated deduction in nonclassical logic","author":"L. Wallen","year":"1990","unstructured":"Wallen, L.: Automated deduction in nonclassical logic. MIT Press, Cambridge (1990)"},{"key":"24_CR30","unstructured":"Weidenbach, C.: SPASS: Combining superposition, sorts and splitting. In: Handbook of Automated Reasoning. Elsevier, Amsterdam (1999)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,19]],"date-time":"2020-04-19T15:21:44Z","timestamp":1587309704000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/10722086_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}