{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:38:38Z","timestamp":1725557918573},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540250517"},{"type":"electronic","value":"9783540322542"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-32254-2_3","type":"book-chapter","created":{"date-parts":[[2010,6,22]],"date-time":"2010-06-22T19:16:54Z","timestamp":1277234214000},"page":"30-45","source":"Crossref","is-referenced-by-count":0,"title":["Rewrite and Decision Procedure Laboratory: Combining Rewriting, Satisfiability Checking, and Lemma Speculation"],"prefix":"10.1007","author":[{"given":"Alessandro","family":"Armando","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Compagna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"663","DOI":"10.1007\/3-540-45744-5_54","volume-title":"Automated Reasoning","author":"A. Armando","year":"2001","unstructured":"Armando, A., Compagna, L., Ranise, S.: System Description: RDL\u2014Rewrite and Decision procedure Laboratory. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 663\u2013669. Springer, Heidelberg (2001)"},{"key":"3_CR2","unstructured":"Armando, A., Ranise, S.: Constraint Contextual Rewriting. In: Proc. of the 2nd Intl. Workshop on First Order Theorem Proving, (FTP 1998) (1998)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/10720084_4","volume-title":"Frontiers of Combining Systems","author":"A. Armando","year":"2000","unstructured":"Armando, A., Ranise, S.: Termination of Constraint Contextual Rewriting. In: Kirchner, H. (ed.) FroCos 2000. LNCS, vol.\u00a01794, pp. 47\u201361. Springer, Heidelberg (2000)"},{"issue":"2","key":"3_CR4","first-page":"124","volume":"7","author":"A. Armando","year":"2001","unstructured":"Armando, A., Ranise, S.: A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. Journal of Universal Computer Science\u00a07(2), 124\u2013140 (2001); Special Issue on Tools for System Design and Verification (FM-TOOLS 2000)","journal-title":"Journal of Universal Computer Science"},{"key":"3_CR5","unstructured":"Bj\u00f8rner, N.S.: Integrating Decision Procedures for Temporal Verification. PhD thesis, Computer Science Department, Stanford University (1998)"},{"key":"3_CR6","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, London (1979)"},{"key":"3_CR7","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":"3_CR8","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Hand. of Theoretical Comp. Science, pp. 243\u2013320 (1990)","DOI":"10.1016\/B978-0-444-88074-1.50011-1"},{"key":"3_CR9","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.: Simplify: the ESC Theorem Prover. Technical report DEC (1996)"},{"key":"3_CR10","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"},{"issue":"4","key":"3_CR11","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 Trans. Soft. Eng.\u00a023(4), 203\u2013213 (1997)","journal-title":"IEEE Trans. Soft. Eng."},{"key":"3_CR12","first-page":"263","volume-title":"Computational Problems in Abstract Algebra","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.E.: Simple word problems in universal algebra. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, Oxford, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/BF00245296","volume":"9","author":"J.-L. Lassez","year":"1992","unstructured":"Lassez, J.-L., Maher, M.J.: On Fourier\u2019s Algorithm\u2019s for Linear Arithmetic Constraints. J. of Automated Reasoning\u00a09, 373\u2013379 (1992)","journal-title":"J. of Automated Reasoning"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Manna, Z.: The STeP Group. STeP: The Stanford Temporal Prover. Technical Report CS-TR-94-1518, Stanford University (June 1994)","DOI":"10.21236\/ADA324036"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Maslov, V., Pugh, W.: Simplifying Polynomial Constraints Over Integers to Make Dependence Analysis More Precise. Technical Report CS-TR-3109.1, Dept. of Computer Science, University of Maryland (1994)","DOI":"10.1007\/3-540-58430-7_64"},{"key":"3_CR16","unstructured":"Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. Technical Report STAN-CS-78-652, Stanford Computer Science Department (April 1978)"},{"key":"3_CR17","series-title":"LNAI","first-page":"748","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A Prototype Verification System. In: Kapur, D. (ed.) CADE 1992. LNCS (LNAI), vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Paulson, L.C.: Proving termination of normalization functions for conditional expressions. J. of Automated Reasoning, 63\u201374 (1986)","DOI":"10.1007\/BF00246023"},{"issue":"1","key":"3_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. J. of the ACM\u00a031(1), 1\u201312 (1984)","journal-title":"J. of the ACM"},{"issue":"1\/2","key":"3_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"}],"container-title":["Lecture Notes in Computer Science","Mechanizing Mathematical Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-32254-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,6]],"date-time":"2020-06-06T01:22:22Z","timestamp":1591406542000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-32254-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540250517","9783540322542"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-32254-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}