{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214507,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":44,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540650744"},{"type":"electronic","value":"9783540496748"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-49674-2_1","type":"book-chapter","created":{"date-parts":[[2007,8,14]],"date-time":"2007-08-14T05:41:54Z","timestamp":1187070114000},"page":"1-27","source":"Crossref","is-referenced-by-count":12,"title":["A Multi-level Approach to Program Synthesis"],"prefix":"10.1007","author":[{"given":"W.","family":"Bibel","sequence":"first","affiliation":[]},{"given":"D.","family":"Korn","sequence":"additional","affiliation":[]},{"given":"C.","family":"Kreitz","sequence":"additional","affiliation":[]},{"given":"F.","family":"Kurucz","sequence":"additional","affiliation":[]},{"given":"J.","family":"Otten","sequence":"additional","affiliation":[]},{"given":"S.","family":"Schmitt","sequence":"additional","affiliation":[]},{"given":"G.","family":"Stolpmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1998,11,18]]},"reference":[{"issue":"1\u20132","key":"1_CR1","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00244462","volume":"16","author":"D. Basin","year":"1996","unstructured":"D. Basin & T. Walsh. A calculus for and termination of rippling. Journal of Automated Reasoning, 16(1\u20132), pp. 147\u2013180, 1996.","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","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, 1985.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"J. Van Benthem Correspondence Theory In D. Gabbay & F. Guenther, eds., Handbook of Philosophical Logic, II, pp. 167\u2013247, Reidel, 1984.","DOI":"10.1007\/978-94-009-6259-0_4"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"W. Bibel. On matrices with connections. Journal of the ACM, 28(633\u2013645), 1981.","DOI":"10.1145\/322276.322277"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"1_CR6","unstructured":"W. Bibel. Toward predicative programming. In M. R. Lowry & R. McCartney, eds., Automating Software Design, pp. 405\u2013424, AAAI Press \/ The MIT Press, 1991."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"W. Bibel, S. Br\u00fcning, U. Egly, T. Rath. Komet. In 12 th Conference on Automated Deduction, LNAI 814, pp. 783\u2013787. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_60"},{"key":"1_CR8","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Design and Implementation of Symbolic Computation Systems","author":"W. Bibel","year":"1996","unstructured":"W. Bibel, D. Korn, C. Kreitz, S. Schmitt. Problem-oriented applications of automated theorem proving. In J. Calmet & C. Limongelli, eds., Design and Implementation of Symbolic Computation Systems, LNCS 1126, Springer Verlag, pp. 1\u201321, 1996."},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, A. Ireland, A. Smaill. Rippling: a heuristic for guiding inductive proofs. ArtiFIcial Intelligence, 1992.","DOI":"10.1016\/0004-3702(93)90079-Q"},{"key":"1_CR10","unstructured":"R. L. Constable, et. al. Implementing Mathematics with the NuPRL proof development system. Prentice Hall, 1986."},{"key":"1_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis & H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201\u2013215, 1960.","journal-title":"Journal of the ACM"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, D. Loveland. A machine program for theorem-proving. Communications of the ACM, 5:394\u2013397, 1962.","journal-title":"Communications of the ACM"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"M. C. Fitting. First-Order Logic and Automated Theorem Proving. Springer Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"G. Gentzen. Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift, 39:176\u2013210, 405\u2013431, 1935.","journal-title":"Mathematische Zeitschrift"},{"key":"1_CR15","unstructured":"P. Jackson. NuPRL\u2019s Metalanguage ML. Reference Manual and User\u2019s Guide, Cornell University, 1994."},{"key":"1_CR16","unstructured":"P. Jackson. The NuPRL Proof Development System, Version 4.1. Reference Manual and User\u2019s Guide, Cornell University, 1994."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"D. Korn & C. Kreitz. Deciding intuitionistic propositional logic via translation into classical logic. In W. McCune, ed., 14 th Conference on Automated Deduction, LNAI 1249, pp. 131\u2013145, Springer Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_15"},{"key":"1_CR18","unstructured":"C. Kreitz. METASYNTHESIS: Deriving Programs that Develop Programs. Thesis for Habilitation, TH Darmstadt, 1992. Forschungsbericht AIDA-93-03."},{"issue":"1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1093\/jigpal\/4.1.75","volume":"4","author":"C. Kreitz","year":"1996","unstructured":"C. Kreitz. Formal mathematics for verifiably correct program synthesis. Journal of the IGPL, 4(1):75\u201394, 1996.","journal-title":"Journal of the IGPL"},{"key":"1_CR20","unstructured":"C. Kreitz. Formal reasoning about communication systems I: Embedding ML into type theory. Technical Report TR 97-1637, Cornell University, 1997."},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"C. Kreitz, H. Mantel, J. Otten, S. Schmitt. Connection-Based Proof Construction in Linear Logic. In W. McCune, ed., 14 th Conference on Automated Deduction, LNAI 1249, pp. 207\u2013221, Springer Verlag, 1997.","DOI":"10.1007\/3-540-63104-6_20"},{"key":"1_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-60939-3_10","volume-title":"5th International Workshop on Logic Program Synthesis and Transformation","author":"C. Kreitz","year":"1996","unstructured":"C. Kreitz, J. Otten, S. Schmitt. Guiding Program Development Systems by a Connection Based Proof Strategy. In M. Proietti, ed., 5th International Workshop on Logic Program Synthesis and Transformation, LNCS 1048, pp. 137\u2013151. Springer Verlag, 1996."},{"key":"1_CR23","unstructured":"F. Kurucz. Realisierung verschiedender Induktionsstrategien basierend auf dem Rippling-Kalk\u00fcl. Diplomarbeit, TH Darmstadt, 1997."},{"key":"1_CR24","doi-asserted-by":"publisher","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_CR25","unstructured":"T. van thanh Liem. Induktion im NuPRL System. Diplomarbeit, TH Darmstadt, 1996."},{"key":"1_CR26","unstructured":"R. C. Moore. Reasoning about Knowledge and Action IJCAI-77, pp 223\u2013227, 1977."},{"issue":"6","key":"1_CR27","doi-asserted-by":"publisher","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, 1(6), pp 691\u2013746, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"J. Otten. ileanTAP: An intuitionistic theorem prover. In Didier Galmiche, ed., International Conference TABLEAUX\u2019 97. LNAI 1227, pp. 307\u2013312, Springer Verlag, 1997.","DOI":"10.1007\/BFb0027422"},{"key":"1_CR29","unstructured":"J. Otten. On the advantage of a non-clausal Davis-Putnam procedure. Forschungsbericht AIDA-97-01, TH Darmstadt, 1997."},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"J. Otten & C. Kreitz. A connection based proof method for intuitionistic logic. In P. Baumgartner, R. H\u00e4hnle, J. Posegga, eds., 4 th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pp. 122\u2013137, Springer Verlag, 1995.","DOI":"10.1007\/3-540-59338-1_32"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"J. Otten & C. Kreitz. T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. In U. Moscato, ed., 5 th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 1071, pp. 244\u2013260, Springer Verlag, 1996.","DOI":"10.1007\/3-540-61208-4_16"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"J. Otten & C. Kreitz. A Uniform Proof Procedure for Classical and Non-classical Logics. In G. G\u00f6rz & S. H\u00f6lldobler, eds., KI-96: Advances in Artificial Intelligence, LNAI 1137, pp. 307\u2013319. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61708-6_70"},{"key":"1_CR33","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"D. Plaisted & S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2:293\u2013304, 1986.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR34","unstructured":"S. Schmitt. Avoiding redundancy in proof reconstruction 1 st International Workshop on Proof Transformation and Presentation, Schlo\u00df Dagstuhl, Germany, 1997."},{"key":"1_CR35","unstructured":"S. Schmitt. Building Efficient Conversion Procedures using Proof Knowledge. Technical Report, TH Darmstadt, 1997."},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"S. Schmitt & C. Kreitz. On transforming intuitionistic matrix proofs into standard-sequent proofs. In P. Baumgartner, R. H\u00e4hnle, J. Posegga, eds., 4 th Workshop on Theorem Proving with Analytic Tableaux and Related Methods, LNAI 918, pp. 106\u2013121. Springer Verlag, 1995.","DOI":"10.1007\/3-540-59338-1_31"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"S. Schmitt & C. Kreitz. Converting non-classical matrix proofs into sequent-style systems. In M. McRobbie & J. Slaney, eds., 13 th Conference on Automated Deduction, LNAI 1104, pp. 418\u2013432. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61511-3_104"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"S. Schmitt & C. Kreitz. A uniform procedure for converting non-classical matrix proofs into sequent-style systems. Technical Report AIDA-96-01, TH Darmstadt 1996.","DOI":"10.1007\/3-540-61511-3_104"},{"key":"1_CR39","unstructured":"D. R. Smith. Structure and design of global search algorithms. Technical Report KES.U.87.12, Kestrel Institute, 1987."},{"issue":"2\u20133","key":"1_CR40","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/0167-6423(90)90025-9","volume":"14","author":"D. R. Smith","year":"1990","unstructured":"D. R. Smith & M. R. Lowry. Algorithm theories and design tactics. Science of Computer Programming, 14(2\u20133):305\u2013321, 1990.","journal-title":"Science of Computer Programming"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"D. R. Smith & E. A. Parra. Transformational approach to transportation scheduling. 8 th Knowledge-Based Software Engineering Conference, pp. 60\u201368, 1993.","DOI":"10.1109\/KBSE.1993.341197"},{"key":"1_CR42","unstructured":"G. Stolpmann. Datentypen und Programmsynthese. Studienarbeit, TH Darmstadt, 1996."},{"key":"1_CR43","unstructured":"G. Stolpmann. Schematische Konstruktion von Globalsuchalgorithmen. Diplomarbeit, TH Darmstadt, 1997."},{"key":"1_CR44","unstructured":"L. Wallen. Automated deduction in nonclassical logic. MIT Press, 1990."}],"container-title":["Lecture Notes in Computer Science","Logic Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49674-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T09:35:51Z","timestamp":1737365751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49674-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540650744","9783540496748"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/3-540-49674-2_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}