{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:16:29Z","timestamp":1725574589201},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203636"},{"type":"electronic","value":"9783540397243"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39724-3_29","type":"book-chapter","created":{"date-parts":[[2011,1,8]],"date-time":"2011-01-08T02:15:55Z","timestamp":1294452955000},"page":"319-333","source":"Crossref","is-referenced-by-count":18,"title":["Linear and Nonlinear Arithmetic in ACL2"],"prefix":"10.1007","author":[{"suffix":"Jr.","given":"Warren A.","family":"Hunt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert Bellarmine","family":"Krug","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J.","family":"Moore","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"29_CR1","first-page":"124","volume":"7","author":"A. Armando","year":"2001","unstructured":"Armando, A., Ranise, S.: A Practical Extension Mechanism for Decision Procedures. Journal of Universal Computer Science\u00a07(2), 124\u2013140 (2001)","journal-title":"Journal of Universal Computer Science"},{"key":"29_CR2","first-page":"83","volume":"11","author":"R. Boyer","year":"1988","unstructured":"Boyer, R., Moore, J.: Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic. Machine Intelligence\u00a011, 83\u2013124 (1988)","journal-title":"Machine Intelligence"},{"key":"29_CR3","unstructured":"Cyrluk, D., Kapur, D.: Reasoning about Nonlinear Inequality Constraints: A Multi-level Approach. In: Proceedings DARPA workshop on Image Understanding, pp. 904\u2013915 (1989)"},{"key":"29_CR4","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers. Technical Report TR-408, University of Cambridge Computer Laboratory (December 1996)"},{"key":"29_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/BFb0028391","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"1997","unstructured":"Harrison, J.: Verifying the Accuracy of Polynomial Approximations in HOL. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 137\u2013152. Springer, Heidelberg (1997)"},{"key":"29_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-45988-X_8","volume-title":"Frontiers of Combining Systems","author":"D. Kapur","year":"2002","unstructured":"Kapur, D.: A Rewrite Rule Based Framework for Combining Decision Procedures. In: Armando, A. (ed.) FroCos 2002. LNCS (LNAI), vol.\u00a02309, pp. 87\u2013102. Springer, Heidelberg (2002)"},{"volume-title":"Computer-Aided Reasoning: An Approach","year":"2000","key":"29_CR7","unstructured":"Kaufmann, M., Manolios, P., Moore, J. (eds.): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"29_CR8","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"29_CR9","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1109\/CMPASS.1996.507872","volume-title":"Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS 1996)","author":"M. Kaufmann","year":"1996","unstructured":"Kaufmann, M., Moore, J.: ACL2: An Industrial Strength Version of Nqthm. In: Proceedings of the Eleventh Annual Conference on Computer Assurance (COMPASS 1996), pp. 23\u201334. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/BFb0031800","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Miner","year":"1996","unstructured":"Miner, P., Leathrum, J.: Verification of IEEE Compliant Subtractive Division Algorithms. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 64\u201378. Springer, Heidelberg (1996)"},{"key":"29_CR11","first-page":"245","volume-title":"ACM Transactions on Programming Languages and Systems (TOPLAS)","author":"G. Nelson","year":"1996","unstructured":"Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. In: ACM Transactions on Programming Languages and Systems (TOPLAS), October 1979, vol.\u00a01(2), pp. 245\u2013257. Springer, Heidelberg (1996)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45610-4_1","volume-title":"Rewriting Techniques and Applications","author":"H. Rue\u00df","year":"2002","unstructured":"Rue\u00df, H., Shankar, N.: Combining Shostak Theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, pp. 1\u201318. Springer, Heidelberg (2002)"},{"key":"29_CR13","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D. Russinoff","year":"1998","unstructured":"Russinoff, D.: A Mechanically Checked Proof of IEEE Compliance of a Register- Transfer-Level Specification of the AMD K7 Floating Point Multiplication, Division and Square Root Instructions. LMS Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998)","journal-title":"LMS Journal of Computation and Mathematics"},{"issue":"1","key":"29_CR14","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. Journal of the ACM (JACM)\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the ACM (JACM)"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39724-3_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,29]],"date-time":"2020-01-29T23:10:17Z","timestamp":1580339417000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39724-3_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203636","9783540397243"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39724-3_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}