{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:06:05Z","timestamp":1749125165735},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540657651"},{"type":"electronic","value":"9783540489580"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48958-4_4","type":"book-chapter","created":{"date-parts":[[2007,7,23]],"date-time":"2007-07-23T02:11:42Z","timestamp":1185156702000},"page":"61-80","source":"Crossref","is-referenced-by-count":4,"title":["Using Decision Procedures to Accelerate Domain-Specific Deductive Synthesis Systems"],"prefix":"10.1007","author":[{"given":"Jeffrey","family":"Van Baalen","sequence":"first","affiliation":[]},{"given":"Steven","family":"Roach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F. & Tinelli, C, \u201cA New Approach for Combining Decision Procedures for the Word Problem, and its Connection to the Nelson-Oppen Combination Method,\u201d CADE14, pp. 19\u201333, 1997.","DOI":"10.1007\/3-540-63104-6_3"},{"key":"4_CR2","unstructured":"R. Boyer and Moore, J, 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, 1988."},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Burckert, H. J., \u201cA Resolution Principle for a Logic With Restricted Quantifiers,\u201d Lecture Notes in Artificial Intelligence, Vol. 568, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-55034-8"},{"key":"4_CR4","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"Chang, C & Lee, R.C., Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"4_CR5","doi-asserted-by":"crossref","unstructured":"Cyrluk, D., Lincoln, P., Shankar, N. \u201cOn Shostak\u2019s decision procedures for combinations of theories,\u201d Automated Deduction\u2014CADE-13 in Lecture Notes in AI 1104, (M. A. McRobbie and J. K. Slaney Eds), Springer, pp. 463\u2013477, 1996.","DOI":"10.1007\/3-540-61511-3_107"},{"key":"4_CR6","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0743-1066(94)90029-9","volume":"19","author":"Y. Deville","year":"1994","unstructured":"Deville, Y. and Lau, K., \u201cLogic Program Synthesis,\u201d Journal of Logic Programming, 19,20: 321\u2013350, 1994.","journal-title":"Journal of Logic Programming"},{"key":"4_CR7","first-page":"173","volume-title":"Proceedings of the Symposium on Mathematical Theory of Automata","author":"B. Dunham","year":"1963","unstructured":"Dunham, B. and North, J., \u201cTheorem Testing by Computer,\u201d Proceedings of the Symposium on Mathematical Theory of Automata, Polytechnic Press, Brooklyn, N.Y., pp. 173\u2013177, 1963."},{"key":"4_CR8","unstructured":"Gallier, J.H., Logic for Computer Science: Foundations of Automatic Theorem Proving, Harper and Row, 1986."},{"key":"4_CR9","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C.A.R. Hoare","year":"1973","unstructured":"C.A.R. Hoare, \u201cProof of Correctness of Data Representations,\u201d Acta Infomatica, Vol. 1, pp. 271\u2013281, 1973.","journal-title":"Acta Infomatica"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1023\/A:1008637201658","volume":"4","author":"M. Lowry","year":"1997","unstructured":"M. Lowry and J. Van Baalen, \u201cMETA-Amphion: Synthesis of Efficient Domain-Specific Program Synthesis Systems\u201d, Automated Software Engineering, vol 4, pp. 199\u2013241, 1997.","journal-title":"Automated Software Engineering"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Nelson, G., and Oppen, D., \u201cSimplification By Cooperating Decision Procedures,\u201d ACM Transactions on Programming Languages and Systems, No. 1, pp. 245\u2013257, 1979.","DOI":"10.1145\/357073.357079"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., and Oppen, D., \u201cFast decision procedures based on congruence closure,\u201d Journal of the ACM, 27, 2, pp. 356\u2013364, 1980.","journal-title":"Journal of the ACM"},{"key":"4_CR13","first-page":"748","volume":"607","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, M., and Shankar, N., \u201cPVS: A Prototype Verification System,\u201d CADE-11, LNAI Vol. 607, pp. 748\u2013752, 1992.","journal-title":"CADE-11"},{"key":"4_CR14","unstructured":"Roach, S., \u201cTOPS: Theory Operationalization for Program Synthesis,\u201d Ph.D. Thesis at University of Wyoming, 1997."},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. Shostak","year":"1979","unstructured":"Shostak, R., \u201cA practical decision procedure for arithmetic with function symbols,\u201d Journal of the ACM, Vol. 26, pp. 351\u2013360, 1979.","journal-title":"Journal of the ACM"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. Shostak","year":"1984","unstructured":"Shostak, R., \u201cDeciding Combinations of Theories,\u201d Journal of the ACM, Vol. 31, pp. 1\u201312, 1984.","journal-title":"Journal of the ACM"},{"key":"4_CR17","doi-asserted-by":"crossref","unstructured":"M. Stickel, R. Waldinger, M. Lowry, T. Pressburger, and I. Underwood, \u201cDeductive Composition of Astronomical Software from Subroutine Libraries,\u201d CADE-12, 1994. See http:\/\/ic-www.arc.nasa.gov\/ic\/projects\/amphion\/docs\/amphion.html","DOI":"10.1007\/3-540-58156-1_24"}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48958-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T11:42:15Z","timestamp":1556710935000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48958-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540657651","9783540489580"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-48958-4_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}