{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:58:57Z","timestamp":1754488737029,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631040"},{"type":"electronic","value":"9783540691402"}],"license":[{"start":{"date-parts":[[1997,1,1]],"date-time":"1997-01-01T00:00:00Z","timestamp":852076800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63104-6_13","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:03:53Z","timestamp":1330279433000},"page":"101-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["A practical integration of first-order reasoning and decision procedures"],"prefix":"10.1007","author":[{"given":"Nikolaj S.","family":"Bj\u00f8rner","sequence":"first","affiliation":[]},{"given":"Mark E.","family":"Stickel","sequence":"additional","affiliation":[]},{"given":"Tom\u00e1s E.","family":"Uribe","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"issue":"2","key":"13_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. B. Andrews","year":"1981","unstructured":"Andrews, P. B. Theorem proving via general matings. J. ACM 28, 2 (Apr. 1981), 193\u2013214.","journal-title":"J. ACM"},{"key":"13_CR2","volume-title":"Handbook of Logic in Artificial Intelligence and Logic Programming","author":"F. Baader","year":"1993","unstructured":"Baader, F., and Siekmann, J. Unification theory. In Handbook of Logic in Artificial Intelligence and Logic Programming, D. Gabbay, C. Hogger, and J. Robinson, Eds. Oxford University Press, Oxford, UK, 1993."},{"key":"13_CR3","unstructured":"Barret, C., Dill, D., and Levitt, J. Validity checking for combinations of theories with equality. In 1st Intl. Conf. on Formal Methods in Computer-Aided Design (Nov. 1996), vol. 1166 of LNCS, pp. 187\u2013201."},{"key":"13_CR4","unstructured":"Baumgartner, P., Furbach, U., and Petermann, U. A unified approach to theory reasoning. Research Report 15\u201392, Fachbereich Informatik, Universit\u00e4t Koblenz, 1992."},{"key":"13_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-322-90100-2","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1982","unstructured":"Bibel, W.Automated Theorem Proving. Friedr. Vieweg & Sohn, Braunschweig, Germany, 1982."},{"key":"13_CR6","unstructured":"Bj\u00f8rner, N., Browne, A., Chang, E., Col\u00f3n, M., Kapur, A., Manna, Z., Sipma, H., and Uribe, T. STeP: Deductive-algorithmic verification of reactive and real-time systems. In Proc. 8thIntl. Conference on Computer Aided Verification (July 1996), vol. 1102 of LNCS, Springer-Verlag, pp. 415\u2013418."},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., Manna, Z., Sipma, H., and Uribe, T. Deductive verification of real-time systems using STeP. In AMAST Workshop on Real-Time Systems (1997), LNCS, Springer-Verlag. To appear.","DOI":"10.1007\/3-540-63010-4_3"},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"B\u00fcrckert, H.-J. A Resolution Principle for a Logic with Restricted Quantifiers, vol. 568 of LNAI. Springer-Verlag, 1991.","DOI":"10.1007\/3-540-55034-8"},{"key":"13_CR9","unstructured":"Clarke, E., German, S., and Zhao, X. Verifying the SRT division algorithm using theorem-proving techniques. In Proc. 8thIntl. Conference on Computer Aided Verification (July 1996), vol. 1102 of LNCS, Springer-Verlag, pp. 111\u2013122."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Cyrluk, D., Lincoln, P., and Shankar, N. On Shostak's decision procedure for combinations of theories. In Proc. 13th Int. Conf. on Automated Deduction (1996), vol. 1104 of LNAI, Springer-Verlag.","DOI":"10.1007\/3-540-61511-3_107"},{"key":"13_CR11","unstructured":"Davis, M. Obvious logical inferences. In Proceedings of the Seventh International Joint Conference on Artificial Intelligence (August 1981), pp. 530\u2013531."},{"issue":"7","key":"13_CR12","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., and Loveland, D. A machine program for theorem-proving. Communications of the ACM 5, 7 (July 1962), 394\u2013397.","journal-title":"Communications of the ACM"},{"key":"13_CR13","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., and Putnam, H. A computing procedure for quantification theory. J. ACM 7 (1960), 201\u2013215.","journal-title":"J. ACM"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Degtyarev, A., and Voronkov, A. Simultaneous rigid E-unification is undecidable. UPMAIL Technical Report No. 105, Computing Science Department, Uppsala University, 1995.","DOI":"10.1007\/3-540-61377-3_38"},{"key":"13_CR15","unstructured":"Detlefs, D. An overview of the extended static checking system. In Proc. First Workshop on Formal Methods in Software Practice (Jan. 1996), ACM (SIGSOFT), pp. 1\u20139."},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0004-3702(91)90009-9","volume":"49","author":"A. M. Frisch","year":"1991","unstructured":"Frisch, A. M. The substitutions a framework for sorted deduction: Fundamental results on hybrid reasoning. Artificial Intelligence 49 (1991), 161\u2013198.","journal-title":"Artificial Intelligence"},{"issue":"2","key":"13_CR17","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1145\/128749.128754","volume":"39","author":"J. Gallier","year":"1992","unstructured":"Gallier, J., Narendran, P., Raatz, S., and Snyder, W. Theorem proving using equational matings and rigid E-unification. J. ACM 39, 2 (Apr. 1992), 377\u2013429.","journal-title":"J. ACM"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/BF00881805","volume":"15","author":"J. N. Hooker","year":"1995","unstructured":"Hooker, J. N., and Vinay, V. Branching rules for satisfiability. J. Automated Reasoning 15 (1995), 359\u2013383.","journal-title":"J. Automated Reasoning"},{"key":"13_CR19","unstructured":"Issar, S. Path-focused duplication: A search procedure for general matings. In Proceedings of the Eighth National Conference on Artificial Intelligence (July\u2013August 1990), pp. 221\u2013226."},{"key":"13_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., and Pnueli, A.Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"13_CR21","volume-title":"The Deductive Foundations of Computer Programming","author":"Z. Manna","year":"1993","unstructured":"Manna, Z., and Waldinger, R.The Deductive Foundations of Computer Programming. Addison-Wesley, Reading, MA, 1993."},{"key":"13_CR22","unstructured":"Nelson, G., and Detlefs, D. ESC pages and Simplify man page. On-line documentation, DEC Systems Research Center, 1996. http:\/\/www.research.digital.com\/SRC\/esc\/Esc.html."},{"issue":"2","key":"13_CR23","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. Fast decision procedures based on congruence closure. J. ACM 27, 2 (Apr. 1980), 356\u2013364.","journal-title":"J. ACM"},{"key":"13_CR24","unstructured":"Owre, S., Rajan, S., Rushby, J., Shankar, N., and Srivas, M. PVS: Combining specification, proof checking, and model checking. In Proc. 8thIntl. Conference on Computer Aided Verification (July 1996), vol. 1102 of LNCS, Springer-Verlag, pp. 411\u2013414."},{"key":"13_CR25","first-page":"73","volume":"57","author":"G. Plotkin","year":"1972","unstructured":"Plotkin, G. Building in equational theories. Machine Intelligence 57 (1972), 73\u201390.","journal-title":"Machine Intelligence"},{"issue":"1","key":"13_CR26","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"Robinson, J. A machine-oriented logic based on the resolution principle. J. ACM 12, 1 (1965), 23\u201341.","journal-title":"J. ACM"},{"issue":"1","key":"13_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R. Shostak","year":"1984","unstructured":"Shostak, R. Deciding combinations of theories. J. ACM 31, 1 (Jan. 1984), 1\u201312.","journal-title":"J. ACM"},{"issue":"4","key":"13_CR28","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. Stickel","year":"1985","unstructured":"Stickel, M. Automated deduction by theory resolution. J. Automated Reasoning 1, 4 (1985), 333\u2013355.","journal-title":"J. Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-14"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63104-6_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:44:04Z","timestamp":1558255444000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63104-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631040","9783540691402"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-63104-6_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]},"assertion":[{"value":"8 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}