{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,24]],"date-time":"2025-05-24T07:47:13Z","timestamp":1748072833023},"publisher-location":"Berlin, Heidelberg","reference-count":12,"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_24","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:21:51Z","timestamp":1330269711000},"page":"341-355","source":"Crossref","is-referenced-by-count":46,"title":["Deductive composition of astronomical software from subroutine libraries"],"prefix":"10.1007","author":[{"given":"Mark","family":"Stickel","sequence":"first","affiliation":[]},{"given":"Richard","family":"Waldinger","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Lowry","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Pressburger","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Underwood","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"24_CR1","volume-title":"A Computational Logic Handbook","author":"R. S. Boyer","year":"1988","unstructured":"R. S. Boyer and J S. Moore, A Computational Logic Handbook, Academic Press, Boston, MA (1988)."},{"issue":"3","key":"24_CR2","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","volume":"17","author":"N. Dershowitz","year":"1982","unstructured":"N. Dershowitz, Orderings for Term-Rewriting Systems, Journal of Theoretical Computer Science, 17, 3 (1982), 279\u2013301.","journal-title":"Journal of Theoretical Computer Science"},{"issue":"3","key":"24_CR3","doi-asserted-by":"crossref","first-page":"559","DOI":"10.1145\/116825.116833","volume":"38","author":"J. Hsiang","year":"1991","unstructured":"J. Hsiang and M. Rusinowitch, Proving Refutation Completeness of Theorem-Proving Strategies: The Transfinite Semantic Tree Method, Journal of the ACM, 38, 3 (1991), 559\u2013587.","journal-title":"Journal of the ACM"},{"key":"24_CR4","volume-title":"Technical Report ANL-90\/9","author":"W. McCune","year":"1990","unstructured":"W. McCune, Otter 2.0 User's Guide, Technical Report ANL-90\/9, Argonne National Laboratory, Argonne, IL (1990)."},{"issue":"8","key":"24_CR5","doi-asserted-by":"crossref","first-page":"674","DOI":"10.1109\/32.153379","volume":"18","author":"Z. Manna","year":"1992","unstructured":"Z. Manna and R. Waldinger, Fundamentals of Deductive Program Synthesis, IEEE Transactions on Software Engineering, 18, 8 (1992), 674\u2013704.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR6","volume-title":"Deductive Foundations of Computer Programming","author":"Z. Manna","year":"1993","unstructured":"Z. Manna and R. Waldinger, Deductive Foundations of Computer Programming, Addison-Wesley, Reading, MA (1993)."},{"key":"24_CR7","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 the ACM 12 (1965) 23\u201341.","journal-title":"Journal of the ACM"},{"key":"24_CR8","unstructured":"E. J. Rollins and J. M. Wing, Specifications as Search Keys for Software Libraries, Eighth International Conference on Logic Programming, Paris, June 1991."},{"issue":"9","key":"24_CR9","doi-asserted-by":"crossref","first-page":"1024","DOI":"10.1109\/32.58788","volume":"16","author":"D. R. Smith","year":"1990","unstructured":"D. R. Smith, KIDS: A Semiautomatic Program Development System. IEEE Transactions on Software Engineering 16, 9 (1990) 1024\u20131043.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"24_CR10","volume-title":"Knowledge-Based Programming","author":"E. H. Tyugu","year":"1988","unstructured":"E. H. Tyugu, Knowledge-Based Programming, Turing Institute Press, Glasgow, Scotland, 1988."},{"key":"24_CR11","first-page":"135","volume-title":"Machine Intelligence 4","author":"L. Wos","year":"1969","unstructured":"L. Wos and G. Robinson, Paramodulation and Theorem Proving in First-Order Theories with Equality. In B. Meltzer and D. Michie (editors), Machine Intelligence 4, American Elsevier, New York, NY (1969) 135\u2013150."},{"issue":"4","key":"24_CR12","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. A. Robinson, and D. F. Carson, Efficiency and Completeness of the Set-of-Support Strategy in Theorem Proving. Journal of the ACM, 12, 4 (1965), 536\u2013541.","journal-title":"Journal of the ACM"}],"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_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:11:51Z","timestamp":1619572311000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}