{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:37:22Z","timestamp":1725493042422},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540422549"},{"type":"electronic","value":"9783540457442"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45744-5_54","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T17:02:07Z","timestamp":1193418127000},"page":"663-669","source":"Crossref","is-referenced-by-count":4,"title":["System Description: RDL Rewrite and Decision Procedure Laboratory"],"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","published-online":{"date-parts":[[2001,6,8]]},"reference":[{"key":"54_CR1","unstructured":"A. Armando and S. Ranise. Constraint Contextual Rewriting. In Proc. of the 2nd Intl. Workshop on First Order Theorem Proving (FTP\u201998), Vienna (Austria), pages 65\u201375, 1998."},{"key":"54_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/10720084_4","volume-title":"Proc. of the 3rd Intl. Workshop on Frontiers of Combining Systems (FroCos\u20192000)","author":"A. Armando","year":"2000","unstructured":"A. Armando and S. Ranise. Termination of Constraint Contextual Rewriting. In Proc. of the 3rd Intl. Workshop on Frontiers of Combining Systems (FroCos\u20192000), LNCS 1794, pages 47\u201361, March 2000."},{"issue":"2","key":"54_CR3","first-page":"124","volume":"7","author":"A. Armando","year":"2001","unstructured":"A. Armando and S. Ranise. A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic. J. of Universal Computer Science (Special Issue: Formal Methods and Tools), 7(2):124\u2013140, 2001.","journal-title":"J. of Universal Computer Science (Special Issue: Formal Methods and Tools)"},{"key":"54_CR4","unstructured":"N. S. Bj\u00f8rner. Integrating Decision Procedures for Temporal Verification. PhD thesis, Computer Science Department, Stanford University, 1998."},{"key":"54_CR5","unstructured":"R.S. Boyer and J S. Moore. A Computational Logic. Academic Press, 1979."},{"key":"54_CR6","first-page":"83","volume":"11","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J S. Moore. Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Machine Intelligence, 11:83\u2013124, 1988.","journal-title":"Machine Intelligence"},{"key":"54_CR7","unstructured":"D. L. Detlefs, G. Nelson, and J. Saxe. Simplify: the ESC Theorem Prover. Technical report, DEC, 1996."},{"key":"54_CR8","doi-asserted-by":"crossref","unstructured":"Z. Manna et. al. STeP: The Stanford Temporal Prover. Technical Report CS-TR-94-1518, Stanford University, June 1994.","DOI":"10.21236\/ADA324036"},{"key":"54_CR9","doi-asserted-by":"crossref","unstructured":"D. Kapur, D.R. Musser, and X. Nie. An Overview of the Tecton Proof System. Theoretical Computer Science, Vol. 133, October 1994.","DOI":"10.1016\/0304-3975(94)90192-9"},{"issue":"4","key":"54_CR10","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M. Kaufmann","year":"1997","unstructured":"M. Kaufmann and J S. Moore. Industrial Strength Theorem Prover for a Logic Based on Common Lisp. IEEE Trans. on Software Engineering, 23(4):203\u2013213, April 1997.","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"2","key":"54_CR11","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D. Oppen. Fast Decision Procedures Based on Congruence Closure. J. of the ACM, 27(2):356\u2013364, April 1980.","journal-title":"J. of the ACM"},{"key":"54_CR12","doi-asserted-by":"crossref","unstructured":"L. C Paulson. Proving termination of normalization functions for conditional expressions. J. of Automated Reasoning, pages 63\u201374, 1986.","DOI":"10.1007\/BF00246023"},{"issue":"1","key":"54_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"R.E. Shostak. Deciding Combination of Theories. Journal of the ACM, 31(1):1\u201312, 1984.","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45744-5_54","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,3]],"date-time":"2019-05-03T21:50:54Z","timestamp":1556920254000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45744-5_54"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540422549","9783540457442"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-45744-5_54","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]}}}