{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:46Z","timestamp":1749124066420},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672814"},{"type":"electronic","value":"9783540464211"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10720084_4","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T14:36:30Z","timestamp":1167402990000},"page":"47-61","source":"Crossref","is-referenced-by-count":5,"title":["Termination of Constraint Contextual Rewriting"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Armando, A., Ranise, S.: Constraint Contextual Rewriting. In: Caferra, R., Salzer, G. (eds.) Proc. of the 2nd Intl. Workshop on First Order Theorem Proving (FTP 1998), Vienna, Austria, November 23-25, pp. 65\u201375 (1998)"},{"key":"4_CR2","unstructured":"Bj\u00f8rner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Computer Science Department, Stanford University (1998)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/3-540-63104-6_13","volume-title":"Automated Deduction - CADE-14","author":"N.S. Bj\u00f8rner","year":"1997","unstructured":"Bj\u00f8rner, N.S., Stickel, M.E., Uribe, T.E.: A practical integration of first-order reasoning and decision procedures. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 101\u2013115. Springer, Heidelberg (1997)"},{"key":"4_CR4","first-page":"83","volume":"11","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Machine Intelligence\u00a011, 83\u2013124 (1988)","journal-title":"Machine Intelligence"},{"key":"4_CR5","unstructured":"Coglio, A., Giunchiglia, F., Pecchiari, P., Talcott, C.L.: A Logic Level Specifica- tion of the NQTHM Simplification Process. Technical report, IRST (1997)"},{"key":"4_CR6","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/3-540-61511-3_107","volume-title":"Automated Deduction - Cade-13","author":"D. Cyrluk","year":"1996","unstructured":"Cyrluk, D., Lincoln, P., Shankar, N.: On Shostak\u2019s decision procedure for combinations of theories. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 463\u2013477. Springer, Heidelberg (1996)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.P.: Rewriting systems. In: Handbook of Theoretical Computer Science, pp. 243\u2013320. Elsevier Publishers, Amsterdam (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"4_CR8","unstructured":"Detlefs, D., Nelson, G., Saxe, J.: Simplify: the ESC Prover. COMPAQ, http:\/\/www.research.digital.com\/SRC\/esc\/Esc.html"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Manna, Z., et al.: STeP: The Stanford Temporal Prover. Technical Report CS-TR- 94-1518, Stanford University (June 1994)","DOI":"10.21236\/ADA324036"},{"key":"4_CR10","unstructured":"Giunchiglia, F., Pecchiari, P., Talcott, C.L.: Reasoning Theories: Towards an Architecture for Open Mechanized Reasoning Systems. Technical Report TR-9409- 15, IRST (November 1994)"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Lassez, J.-L.: Constraint logic programming. In: Proceedings 14th ACM Symposium on Principles of Programming Languages, pp. 111\u2013119 (1987)","DOI":"10.1145\/41625.41635"},{"key":"4_CR12","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-48660-7_9","volume-title":"Automated Deduction - CADE-16","author":"P. Jani\u010di\u0107","year":"1999","unstructured":"Jani\u010di\u0107, P., Bundy, A., Green, I.: A framework for the flexible integration of a class of decision procedures into theorem provers. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 127\u2013141. Springer, Heidelberg (1999)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Kapur, D., Musser, D.R., Nie, X.: An Overview of the Tecton Proof System. Theoretical Computer Science\u00a0133 (October 1994)","DOI":"10.1016\/0304-3975(94)90192-9"},{"key":"4_CR14","unstructured":"Kapur, D., Nie, X.: Reasoning about Numbers in Tecton. Technical report, Department of Computer Science, State University of New York, Albany, NY 12222 (March 1994)"},{"issue":"4","key":"4_CR15","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.S.: Industrial strength theorem prover for a logic based on Common Lisp. IEEE Transactions on Software Engineering\u00a023(4), 203\u2013213 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"4_CR16","unstructured":"Klop, J.W.: Term rewriting systems. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol.\u00a02, ch. 1, pp. 1\u2013117. Oxford University Press, Oxford (1992)"},{"key":"4_CR17","unstructured":"Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. Technical Report STAN-CS-78-652, Stanford Computer Science Department (April 1978)"},{"issue":"2","key":"4_CR18","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast Decision Procedures Based on Congruence Closure. Journal of the ACM\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the ACM"},{"issue":"1","key":"4_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding Combination of Theories. Journal of the ACM\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"issue":"1\/2","key":"4_CR20","doi-asserted-by":"crossref","first-page":"107","DOI":"10.3233\/FI-1995-24125","volume":"24","author":"H. Zhang","year":"1995","unstructured":"Zhang, H.: Contextual Rewriting in Automated Reasoning. Fundamenta Informaticae\u00a024(1\/2), 107\u2013123 (1995)","journal-title":"Fundamenta Informaticae"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1007\/3-540-15976-2_2","volume-title":"Rewriting Techniques and Applications","author":"H. Zhang","year":"1985","unstructured":"Zhang, H., Remy, J.L.: Contextual rewriting. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol.\u00a0202, pp. 46\u201362. Springer, Heidelberg (1985)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10720084_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,19]],"date-time":"2020-04-19T15:15:45Z","timestamp":1587309345000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10720084_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672814","9783540464211"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/10720084_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}