{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T20:15:43Z","timestamp":1649189743534},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2005,10,1]],"date-time":"2005-10-01T00:00:00Z","timestamp":1128124800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Software Eng"],"published-print":{"date-parts":[[2005,10]]},"DOI":"10.1007\/s10515-005-2646-6","type":"journal-article","created":{"date-parts":[[2005,7,14]],"date-time":"2005-07-14T17:08:44Z","timestamp":1121360924000},"page":"393-414","source":"Crossref","is-referenced-by-count":3,"title":["Automated Procedure Construction for Deductive Synthesis"],"prefix":"10.1007","volume":"12","author":[{"given":"Steve","family":"Roach","sequence":"first","affiliation":[]},{"given":"Jeffrey","family":"Van Baalen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2646_CR1","first-page":"19","volume":"14","author":"F. Baader","year":"1997","unstructured":"Baader, F. and Tinelli, C. 1997. A new approach for combining decision procedures for the word problem, and its connection to the nelson-oppen combination method. CADE 14: 19\u201333.","journal-title":"CADE"},{"key":"2646_CR2","unstructured":"Barrett, C. 2000. A framework for cooperating decision procedures, CADE 17 in Lecture Notes in Artificial Intelligence. Springer-Verlag, Vol. 1831."},{"key":"2646_CR3","unstructured":"Boyer, R. and Moore, J. 1985. Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Institute for Computing Science and Computer Applications, University of Texas as Austin."},{"key":"2646_CR4","doi-asserted-by":"crossref","unstructured":"B\u00fcrckert, H. J. 1991. A resolution principle for a logic with restricted quantifiers, Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol. 568.","DOI":"10.1007\/3-540-55034-8"},{"key":"2646_CR5","volume-title":"Symbolic Logic and Mechanical Theorem Proving. Inc","author":"C. Chang","year":"1973","unstructured":"Chang, C. and Lee, R. 1973. Symbolic Logic and Mechanical Theorem Proving. Inc., San Diego: Academic Press."},{"key":"2646_CR6","unstructured":"Cyrluk, D., Lincoln, P., and Shankar, N. 1996. On shostak\u2019s decision procedures for combinations of theories, CADE 13 in Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol. 1104: 463\u2013477."},{"key":"2646_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1996","unstructured":"Fitting, M. 1996. First-Order Logic and Automated Theorem Proving. Springer, New York."},{"key":"2646_CR8","unstructured":"Ford, J. and Shankar, N. 2002. Formal verification of a combination decision procedure, CADE 18 in Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol. 2392, pp. 347\u2013362."},{"key":"2646_CR9","unstructured":"Ganzinger, H. 2002. Shostak light, CADE 18 in Lecture Notes in Artificial Intelligence. Springer-Verlag, Vol. 2392, pp. 332\u2013346."},{"key":"2646_CR10","first-page":"219","volume":"69","author":"C. Green","year":"1969","unstructured":"Green, C. 1969. Applications of theorem proving, IJCAI 69: 219\u2013239.","journal-title":"IJCAI"},{"key":"2646_CR11","unstructured":"Goel, A. 1991. Knowledge compilation: A symposium. IEEE Expert, April, pp. 71\u201393."},{"issue":"1","key":"2646_CR12","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1145\/321738.321748","volume":"20","author":"J. Dixon","year":"1973","unstructured":"Dixon, J. 1973. Z-Resolution: Theorem proving with compiled axioms, Journal of the ACM, 20(1), pp. 127\u2013147.","journal-title":"Journal of the ACM"},{"key":"2646_CR13","volume-title":"Partial Evaluation, and Automatic Program Generation","author":"N. Jones","year":"1993","unstructured":"Jones, N., Gomard, C., and Sestoft, P. 1993. Partial Evaluation, and Automatic Program Generation. Prentice Hall, New York."},{"key":"2646_CR14","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1109\/64.79715","volume":"April","author":"R. Keller","year":"1991","unstructured":"Keller, R. 1991. Applying knowledge compilation techniques to model-based reasoning. IEEE Expert, April: 82\u201387.","journal-title":"IEEE Expert"},{"key":"2646_CR15","unstructured":"Komorowski, J. 1991. Synthesis of programs in the partial deduction framework. In M. Lowry and R. McCartney, editors Automating Software Design. AAAI Press, pp. 377\u2013403."},{"key":"2646_CR16","unstructured":"Komorowski, J. 1992. An introduction to partial deduction framework, In Meta-Programming in Logic, Lecture Notes in Artificial Intelligence, Springer-Verlag, Vol. 649, pp. 49\u201369."},{"key":"2646_CR17","doi-asserted-by":"crossref","unstructured":"Lowry, M., Philpot, A., Pressburger, T., and Underwood, I. 1994. A formal approach to domain-oriented software design environments.\u201d KBSE.","DOI":"10.1109\/KBSE.1994.342678"},{"key":"2646_CR18","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1023\/A:1008637201658","volume":"4","author":"M. Lowry","year":"1997","unstructured":"Lowry, M. and Van Baalen, J. 1997. META-Amphion: Synthesis of efficient domain-specific program synthesis systems, Automated Software Engineering, 4: 199\u2013241.","journal-title":"Automated Software Engineering"},{"key":"2646_CR19","unstructured":"Madden, P. and Bundy, A. 1993. General techniques for automatic program optimization and synthesis through theorem proving, Proceedings of EWAIC\u201993."},{"issue":"1","key":"2646_CR20","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1145\/357084.357090","volume":"2","author":"Z. Manna","year":"1980","unstructured":"Manna, Z. and Waldinger, R. 1980. A deductive approach to program synthesis, ACM Transactions on Programming Languages and Systems, 2(1): 90\u2013121.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"2646_CR21","unstructured":"Navigation and Ancillary Information Facility (NAIF). SPICE, http:\/\/pds.jpl.nasa.gov\/naif.html."},{"key":"2646_CR22","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G. and Oppen, D. 1979. Simplification by cooperating decision procedures, ACM Transactions on Programming Languages and Systems, 1: 245\u2013257.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"2646_CR23","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G. and Oppen, D. 1980. Fast decision procedures based on congruence closure, Journal of the ACM, 27(2): 356\u2013364.","journal-title":"Journal of the ACM"},{"key":"2646_CR24","unstructured":"Owre, S., Rushby, M., and Shankar, N. 1992. PVS: A prototype verification system. CADE 11 in Lecture Notes in Artificial Intelligence. Springer-Verlag, Vol. 607, pp. 748\u2013752."},{"key":"2646_CR25","first-page":"153","volume-title":"Machine Intelligence 5","author":"G. Plotkin","year":"1970","unstructured":"Plotkin, G. 1970. A note on inductive generalisation, In M. Meltzer and D. Michie, editors, Machine Intelligence 5. New York: Elsevier North-Holland, pp. 153\u2013163."},{"issue":"8","key":"2646_CR26","doi-asserted-by":"crossref","first-page":"40","DOI":"10.1109\/2.75","volume":"21","author":"C. Rich","year":"1988","unstructured":"Rich, C. and Waters, R. 1988. Automatic programming: Myths and prospects, IEEE Computer, 21(8): 40\u201351.","journal-title":"IEEE Computer"},{"key":"2646_CR27","unstructured":"Roach, S. 2002. Logic-based program synthesis: State-of-the-Art and future trends.\u201d In Proceedings of the 2002 American Association for Artificial Intelligence AAAI Spring Symposium on Logic-Based Program Synthesis. California: March, Stanford University, Palo Alto."},{"key":"2646_CR28","unstructured":"Roach, S., Lowry, M., and Pressburger, T. 1995. Animating observation geometries with amphion, NASA Information Systems Newsletter, III: 35."},{"key":"2646_CR29","unstructured":"Roach, S. 1997. TOPS: Theory operationalization for program synthesis.\u201d Ph.D. Theiss at University of Wyoming."},{"key":"2646_CR30","unstructured":"Roach, S., Van Baalen, J., and Lowry, M. 1997. Meta-amphion: Scaling up high assurance deductive program synthesis. In IEEE High Integrity Software Symposium, Albuquerque, New Mexico, October 15\u201316, pp. 81\u201393."},{"issue":"2","key":"2646_CR31","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/226643.226644","volume":"43","author":"B. Selman","year":"1996","unstructured":"Selman, B. and Kautz, H. 1996. Knowledge compilation and theory approximation. JACM, 43(2): 193\u2013224.","journal-title":"JACM"},{"key":"2646_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. Shostak","year":"1984","unstructured":"Shostak, R. 1984. Deciding combinations of theories. Journal of the ACM, 31: 1\u201312.","journal-title":"Journal of the ACM"},{"key":"2646_CR33","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"Stickel, M. 1985. Automated deduction by theory resolution. Journal of Automated Reasoning, 1: 333\u2013355.","journal-title":"Journal of Automated Reasoning"},{"key":"2646_CR34","unstructured":"Stickel, M. 2000. \u201cSNARK\u2013SRI\u2019s New Automated Reasoning Kit.\u201d http:\/\/www.ai.sri.com\/stickel\/snark.html."},{"key":"2646_CR35","doi-asserted-by":"crossref","unstructured":"Stickel, M., Waldinger, R., Lowry, M., Pressburger, T., and Underwood, I. 1994. Deductive composition of astronomical software from subroutine libraries. CADE-12.","DOI":"10.1007\/3-540-58156-1_24"},{"key":"2646_CR36","doi-asserted-by":"crossref","unstructured":"Tinelli, C. and Harandi, M. 1996. A new correctness proof of the nelson-oppen combination procedure. In Proceedings of the 1st International Workshop Frontiers of Combining Systems\u2019.","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"2646_CR37","unstructured":"Van Baalen, J. 1991. The completeness of DRAT, A technique for automatic design of satisfiability procedures. International Conference of Knowledge Representation and Reasoning."},{"key":"2646_CR38","doi-asserted-by":"crossref","unstructured":"Van Baalen, J. 1992. Automated design of specialized representations, Artificial Intelligence, Vol. 54.","DOI":"10.1016\/0004-3702(92)90089-G"},{"key":"2646_CR39","doi-asserted-by":"crossref","unstructured":"Van Baalen, J. and Roach, S. 1999. Using decision procedures to accelerate domain-specific deductive synthesis systems. In P. Flener, editor, Proceedings of the 8th International Workshop on Logic Programming Synthesis and Transformation (LOPSTR\u201998), Manchester, UK, Lecture Notes in Computer Science, Springer-Verlag, Vol. 1559, pp. 61\u201370.","DOI":"10.1007\/3-540-48958-4_4"},{"issue":"1","key":"2646_CR40","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/69.124897","volume":"4","author":"C. Youn","year":"1992","unstructured":"Youn, C., Kim, H., Henschen, L., and Han, J. 1992. Classification and compilation of linear recursive queries in deductive databases, IEEE Transactions on Knowledge and Data Engineering, 4(1): 52.","journal-title":"IEEE Transactions on Knowledge and Data Engineering"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-005-2646-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-005-2646-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-005-2646-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,8]],"date-time":"2020-04-08T07:28:50Z","timestamp":1586330930000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-005-2646-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,10]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,10]]}},"alternative-id":["2646"],"URL":"https:\/\/doi.org\/10.1007\/s10515-005-2646-6","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,10]]}}}