{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:03Z","timestamp":1749124083448},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_3","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:22:26Z","timestamp":1330269746000},"page":"29-41","source":"Crossref","is-referenced-by-count":6,"title":["Synthesis of induction orderings for existence proofs"],"prefix":"10.1007","author":[{"given":"Dieter","family":"Hutter","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Biundo et al. The Karlsruhe Induction Theorem Proving System. 8th CADE, LNCS 230, Springer, 1986","DOI":"10.1007\/3-540-16780-3_132"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Biundo, S. Automatische Synthese rekursiver Programme als Beweisverfahren. Springer, IFB302, 1992","DOI":"10.1007\/978-3-642-84744-8"},{"key":"3_CR3","unstructured":"Boyer, R.S. Moore J S. A Computational Logic. Academic Press, 1979"},{"key":"3_CR4","unstructured":"Bundy, A. et al. The Use of Explicit Plans to Guide Inductive Proofs. 9th CADE, LNAI 310, Springer-Verlag, 1988"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Bundy, A. et al. Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs. 10th CADE, LNAI 449, Springer, 1990","DOI":"10.1007\/3-540-52885-7_84"},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Hesketh, J. et al. Using Middle-Out Reasoning to Control the Synthesis of Tail-Recursive Programs. 11th CADE, LNAI 607, Springer, 1992","DOI":"10.1007\/3-540-55602-8_174"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Hutter, D. Guiding Induction Proofs. 10th CADE, LNAI 449, Springer, 1990","DOI":"10.1007\/3-540-52885-7_85"},{"key":"3_CR8","unstructured":"Hutter, D. Mustergesteuerte Strategien f\u00fcr das Beweisen von Gleichheiten. Ph.D. thesis, University of Karlsruhe, 1991"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Manna, Z.; Waldinger, R. A Deductive Approach to Program Synthesis. ACM Transactions on Programming Languages and Systems, Vol. 2 No. 1, 1980","DOI":"10.1145\/357084.357090"},{"key":"3_CR10","unstructured":"Stevens, A. A Rational Reconstruction of Boyer and Moore's Technique for Constructing Induction Formulas. Proceeding of ECAI88, 1988"},{"key":"3_CR11","unstructured":"Walther, C. Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. 9th CADE, LNCS310, Springer, 1988"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:37Z","timestamp":1605647857000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}