{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:51Z","timestamp":1749124071230},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_9","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"127-141","source":"Crossref","is-referenced-by-count":3,"title":["A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers"],"prefix":"10.1007","author":[{"given":"Predrag","family":"Jani\u010di\u0107","sequence":"first","affiliation":[]},{"given":"Alan","family":"Bundy","sequence":"additional","affiliation":[]},{"given":"Ian","family":"Green","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"L. Bachmair and H. Ganzinger. Strict basic superposition. In Kirchner and Kirchner [12], pages 160\u2013174.","key":"9_CR1","DOI":"10.1007\/BFb0054258"},{"doi-asserted-by":"crossref","unstructured":"L. Bachmair, H. Ganzinger, and A. Voronkov. Elimination of equality via transformation with ordering constraints. In Kirchner and Kirchner [12], pages 175\u2013190.","key":"9_CR2","DOI":"10.1007\/BFb0054259"},{"unstructured":"R. S. Boyer and J S. Moore. Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In J. E. Hayes, J. Richards, and D. Michie, editors, Machine Intelligence 11, pages 83\u2013124, 1988.","key":"9_CR3"},{"doi-asserted-by":"crossref","unstructured":"A. Bundy. The use of proof plans for normalization. In R. S. Boyer, editor, Essays in Honor of Woody Bledsoe, pages 149\u2013166. Kluwer, 1991.","key":"9_CR4","DOI":"10.1007\/978-94-011-3488-0_7"},{"doi-asserted-by":"crossref","unstructured":"A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M. E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647\u2013648. Springer-Verlag, 1990..","key":"9_CR5","DOI":"10.1007\/3-540-52885-7_123"},{"unstructured":"D. C. Cooper. Theorem proving in arithmetic without multiplication. In B. Meltzer and D. Michie, editors, Machine Intelligence 7, pages 91\u201399. Edinburgh University Press, 1972.","key":"9_CR6"},{"doi-asserted-by":"crossref","unstructured":"D. Cyrluk, P. Lincoln, and N. Shankar. On Shostak\u2019s decision procedure for combinations of theories. In M. McRobbie and J. Slaney,editors, 13th International Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, Vol. 1104, New Brunswick, NJ, USA, 1996. Springer-Verlag.","key":"9_CR7","DOI":"10.1007\/3-540-61511-3_107"},{"unstructured":"User guide for the Ehdm specification language and verification system, version 6.1. Technical report, SRI Computer Science Laboratory, 1993.","key":"9_CR8"},{"unstructured":"L. Hodes. Solving problems by formula manipulation in logic and linear inequalities. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 553\u2013559, Imperial College, London, England, 1971. The British Computer Society.","key":"9_CR9"},{"unstructured":"P. Jani\u010di\u0107, I. Green, and A. Bundy. A comparison of decision procedures in Presburger arithmetic. In R. To\u0161i\u0107 and Z. Budimac, editors, Proceedings of the VIII Conference on Logic and Computer Science (LIRA\u2019 97), pages 91\u2013101, Novi Sad, Yugoslavia, September 1-4 1997. University of Novi Sad.","key":"9_CR10"},{"unstructured":"D. Kapur and X. Nie. Reasoning about numbers in Tecton. In Proceedings of 8th International Symposium on Methodologies for Intelligent Systems, Charlotte, North Carolina, USA, October 1994.","key":"9_CR11"},{"doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner, editors. 15th International Conference on Automated Deduction, Lindau, Germany, July 1998.","key":"9_CR12","DOI":"10.1007\/BFb0054239"},{"unstructured":"G. Kreisel and J. L. Krivine. Elements of mathematical logic: Model theory. North Holland, Amsterdam, 1967.","key":"9_CR13"},{"doi-asserted-by":"crossref","unstructured":"D. C. Luckham, S. M. German, F. W. von Henke, R. A. Karp, P. W. Milne, D. C. Oppen, W. Polak, and W. L. Scherlis. Stanford Pascal verifier user manual. CSD Report STAN-CS-79-731, Stanford University, 1979.","key":"9_CR14","DOI":"10.21236\/ADA071900"},{"doi-asserted-by":"crossref","unstructured":"Z. Manna et al. STeP: The Stanford Temporal Prover. Technical Report STANCSTR;94-1518, Stanford University, 1994.","key":"9_CR15","DOI":"10.21236\/ADA324036"},{"issue":"2","key":"9_CR16","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u2013257, October 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"9_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Proceedings of the 1996 Conference on Computer-Aided Verification","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger, editors, Proceedings of the 1996 Conference on Computer-Aided Verification, number 1102in LNCS, pages 411\u2013414, New Brunswick, New Jersey, U. S. A., 1996. Springer-Verlag."},{"key":"9_CR18","first-page":"92","volume":"395","author":"M. Presburger","year":"1930","unstructured":"M. Presburger. \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu metematyk\u00f3w slowia\u0144skich, Warszawa 1929, pages 92\u2013101, 395. Warsaw, 1930. Annotated English version also available [20].","journal-title":"Sprawozdanie z I Kongresu metematyk\u00f3w slowia\u0144skich, Warszawa 1929"},{"issue":"1","key":"9_CR19","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 combinations of theories. Journal of the ACM, 31(1):1\u201312, January 1984.","journal-title":"Journal of the ACM"},{"unstructured":"R. Stansifer. Presburger\u2019;s article on integer arithmetic: Remarks and translation. Technical Report TR 84-639, Department of Computer Science, Cornell University, September 1984.","key":"9_CR20"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T08:56:32Z","timestamp":1556960192000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}