{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T17:33:10Z","timestamp":1725471190411},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540371878"},{"type":"electronic","value":"9783540371885"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11814771_43","type":"book-chapter","created":{"date-parts":[[2006,10,5]],"date-time":"2006-10-05T15:44:21Z","timestamp":1160063061000},"page":"528-540","source":"Crossref","is-referenced-by-count":10,"title":["Verifying Mixed Real-Integer Quantifier Elimination"],"prefix":"10.1007","author":[{"given":"Amine","family":"Chaieb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"43_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1017\/S0956796803004921","volume":"14","author":"A.W. Appel","year":"2004","unstructured":"Appel, A.W., Felty, A.P.: Dependent types ensure partial correctness of theorem provers. J. Funct. Program\u00a014(1), 3\u201319 (2004)","journal-title":"J. Funct. Program"},{"key":"43_CR2","unstructured":"Barendregt, H.: Reflection and its use: from science to meditation (2002)"},{"issue":"3","key":"43_CR3","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H. Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. Autom. Reasoning\u00a028(3), 321\u2013336 (2002)","journal-title":"J. Autom. Reasoning"},{"key":"43_CR4","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-44659-1_2","volume-title":"Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics","author":"B. Barras","year":"2000","unstructured":"Barras, B.: Programming and computing in HOL. In: Proceedings of the 13th International Conference on Theorem Proving in Higher Order Logics, pp. 17\u201337. Springer, Heidelberg (2000)"},{"key":"43_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/3-540-36577-X_38","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Berezin","year":"2003","unstructured":"Berezin, S., Ganesh, V., Dill, D.L.: An online proof-producing decision procedure for mixed-integer linear arithmetic. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol.\u00a02619, pp. 521\u2013536. Springer, Heidelberg (2003)"},{"key":"43_CR6","unstructured":"Berghofer, S.: Towards generating proof producing code from HOL definitions. Private communication"},{"key":"43_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45842-5_2","volume-title":"Types for Proofs and Programs","author":"S. Berghofer","year":"2002","unstructured":"Berghofer, S., Nipkow, T.: Executing higher order logic. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 24\u201340. Springer, Heidelberg (2002)"},{"key":"43_CR8","series-title":"Text in theor. comp. science: an EATCS series","volume-title":"Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Coq\u2019Art: The Calculus of Inductive Constructions. Text in theor. comp. science: an EATCS series, vol.\u00a0XXV. Springer, Heidelberg (2004)"},{"issue":"3","key":"43_CR9","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1145\/1071596.1071601","volume":"6","author":"B. Boigelot","year":"2005","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: An effective decision procedure for linear arithmetic over the integers and reals. ACM Trans. Comput. Log.\u00a06(3), 614\u2013633 (2005)","journal-title":"ACM Trans. Comput. Log."},{"key":"43_CR10","unstructured":"Chaieb, A., Nipkow, T.: Generic proof synthesis for presburger arithmetic. Technical report, Technische Universit\u00e4t M\u00fcnchen (2003)"},{"key":"43_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11591191_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"A. Chaieb","year":"2005","unstructured":"Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for Presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, Springer, Heidelberg (2005)"},{"key":"43_CR12","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol.\u00a07, pp. 91\u2013100. Edinburgh University Press (1972)"},{"key":"43_CR13","unstructured":"Cr\u00e9gut, P.: Une proc\u00e9dure de d\u00e9cision r\u00e9flexive pour un fragment de l\u2019arithm\u00e9tique de Presburger. In: Informal proceedings of the 15th journ\u00e9es francophones des langages applicatifs (2004) (In French)"},{"key":"43_CR14","unstructured":"Davis, M.: A computer program for presburger\u2019s algorithm. In: Summaries of talks presented at the Summer Inst. for Symbolic Logic, Cornell University, Inst. for Defense Analyses, Princeton, NJ, pp. 215\u2013233 (1957)"},{"issue":"1","key":"43_CR15","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1137\/0204006","volume":"4","author":"J. Ferrante","year":"1975","unstructured":"Ferrante, J., Rackoff, C.: A decision procedure for the first order theory of real addition with order. SIAM J. Comput.\u00a04(1), 69\u201376 (1975)","journal-title":"SIAM J. Comput."},{"key":"43_CR16","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0062837","volume-title":"The Computational Complexity of Logical Theories","author":"J. Ferrante","year":"1979","unstructured":"Ferrante, J., Rackoff, C.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol.\u00a0718. Springer, Heidelberg (1979)"},{"key":"43_CR17","unstructured":"Fischer, R.: Super-exponential complexity of presburger arithmetic. In: SIAMAMS: Complexity of Computation: Proc. of a Symp. in Appl. Math. of the AMS and the Society for Industrial and Applied Mathematics (1974)"},{"key":"43_CR18","unstructured":"Fourier, J.: Solution d\u2019une question particuli\u00e8re du calcul des inegalit\u00e9s. Nouveau Bulletin des Sciences par la Scoci\u00e9t\u00e9 Philomatique de Paris, pp. 99\u2013100 (1823)"},{"key":"43_CR19","unstructured":"Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995), http:\/\/www.cl.cam.ac.uk\/users\/jrh\/papers\/reflect.dvi.gz"},{"key":"43_CR20","unstructured":"Harrison, J.R.: Introduction to logic and theorem proving (to appear)"},{"key":"43_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/BFb0012835","volume-title":"9th International Conference on Automated Deduction","author":"D.J. Howe","year":"1988","unstructured":"Howe, D.J.: Computational Metatheory in Nuprl. In: Lusk, E.L., Overbeek, R.A. (eds.) CADE 1988. LNCS, vol.\u00a0310, pp. 238\u2013257. Springer, Heidelberg (1988)"},{"key":"43_CR22","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1109\/LICS.2004.1319605","volume-title":"Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004)","author":"F. Klaedtke","year":"2004","unstructured":"Klaedtke, F.: On the automata size for Presburger arithmetic. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS 2004), pp. 110\u2013119. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"43_CR23","unstructured":"Klapper, R., Stump, A.: Validated Proof-Producing Decision Procedures. In: Tinelli, C., Ranise, S. (eds.) 2nd Int. Workshop Pragmatics of Decision Procedures in Automated Reasoning (2004)"},{"issue":"5","key":"43_CR24","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1093\/comjnl\/36.5.450","volume":"36","author":"R. Loos","year":"1993","unstructured":"Loos, R., Weispfenning, V.: Applying linear quantifier elimination. Comput. J.\u00a036(5), 450\u2013462 (1993)","journal-title":"Comput. J."},{"key":"43_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/11532231_22","volume-title":"Automated Deduction \u2013 CADE-20","author":"S. McLaughlin","year":"2005","unstructured":"McLaughlin, S., Harrison, J.: A proof-producing decision procedure for real arithmetic. . In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 295\u2013314. Springer, Heidelberg (2005)"},{"key":"43_CR26","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","author":"S. McLauglin","year":"2006","unstructured":"McLauglin, S.: An Interpretation of Isabelle\/HOL in HOL Light. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"43_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002), http:\/\/www.in.tum.de\/~nipkow\/LNCS2283\/"},{"key":"43_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/10930755_5","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Norrish","year":"2003","unstructured":"Norrish, M.: Complete integer decision procedures as derived rules in HOL. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 71\u201386. Springer, Heidelberg (2003)"},{"key":"43_CR29","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_27","volume-title":"Automated Reasoning","author":"S. Obua","year":"2006","unstructured":"Obua, S., Skalberg, S.: Importing HOL into Isabelle\/HOL. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"43_CR30","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1145\/800125.804033","volume-title":"STOC 1973: Proceedings of the fifth annual ACM symposium on Theory of computing","author":"D.C. Oppen","year":"1973","unstructured":"Oppen, D.C.: Elementary bounds for presburger arithmetic. In: STOC 1973: Proceedings of the fifth annual ACM symposium on Theory of computing, pp. 34\u201337. ACM Press, New York (1973)"},{"key":"43_CR31","unstructured":"Presburger, M.: \u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Comptes Rendus du I Congr\u00e8s des Math. des Pays Slaves, pp. 92\u2013101 (1929)"},{"key":"43_CR32","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1145\/125826.125848","volume-title":"Proceedings of the 1991 ACM\/IEEE conference on Supercomputing","author":"W. Pugh","year":"1991","unstructured":"Pugh, W.: The Omega test: a fast and practical integer programming algorithm for dependence analysis. In: Proceedings of the 1991 ACM\/IEEE conference on Supercomputing, pp. 4\u201313. ACM Press, New York (1991)"},{"key":"43_CR33","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/800133.804361","volume-title":"STOC 1978: Proceedings of the tenth annual ACM symposium on Theory of computing","author":"C.R. Reddy","year":"1978","unstructured":"Reddy, C.R., Loveland, D.W.: Presburger arithmetic with bounded quantifier alternation. In: STOC 1978: Proceedings of the tenth annual ACM symposium on Theory of computing, pp. 320\u2013325. ACM Press, New York (1978)"},{"key":"43_CR34","unstructured":"Skolem, T.: \u00dcber einige Satzfunktionen in der Arithmetik. In: Skrifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I. Matematisk naturvidenskapelig klasse, volume\u00a07, pp. 1\u201328. Oslo (1931)"},{"key":"43_CR35","doi-asserted-by":"crossref","unstructured":"Tarski, A.: A Decision Method for Elementary Algebra and Geometry, 2nd edn. University of California Press (1951)","DOI":"10.1525\/9780520348097"},{"issue":"1\/2","key":"43_CR36","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0747-7171(88)80003-8","volume":"5","author":"V. Weispfenning","year":"1988","unstructured":"Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput.\u00a05(1\/2), 3\u201327 (1988)","journal-title":"J. Symb. Comput."},{"issue":"5","key":"43_CR37","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1016\/S0747-7171(08)80051-X","volume":"10","author":"V. Weispfenning","year":"1990","unstructured":"Weispfenning, V.: The complexity of almost linear diophantine problems. J. Symb. Comput.\u00a010(5), 395\u2013404 (1990)","journal-title":"J. Symb. Comput."},{"key":"43_CR38","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/309831.309888","volume-title":"ISSAC \u201999: Proceedings of the 1999 international symposium on Symbolic and algebraic computation","author":"V. Weispfenning","year":"1999","unstructured":"Weispfenning, V.: Mixed real-integer linear quantifier elimination. In: ISSAC \u201999: Proceedings of the 1999 international symposium on Symbolic and algebraic computation, pp. 129\u2013136. ACM Press, New York (1999)"},{"key":"43_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/3-540-60360-3_30","volume-title":"Static Analysis","author":"P. Wolper","year":"1995","unstructured":"Wolper, P., Boigelot, B.: An automata-theoretic approach to presburger arithmetic constraints (extended abstract). In: Mycroft, A. (ed.) SAS 1995. LNCS, vol.\u00a0983, pp. 21\u201332. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814771_43","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T22:01:56Z","timestamp":1627855316000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814771_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540371878","9783540371885"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/11814771_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}