{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:56:41Z","timestamp":1781884601925,"version":"3.54.5"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031999833","type":"print"},{"value":"9783031999840","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T00:00:00Z","timestamp":1753833600000},"content-version":"vor","delay-in-days":210,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Quantifier elimination is used in various automated reasoning tasks, including quantified SMT solving, exists\/forall solving, program synthesis, model checking, and constrained Horn clause (CHC) solving. Complete quantifier elimination, however, is computationally intractable for many theories. The recent algorithm QEL shows a promising approach to approximate quantifier elimination, which has resulted in improvements in solver performance. QEL performs partial quantifier elimination with a completeness guarantee that depends on a certain semantic property of the given formula. Considerably generalizing the previous approach, we identify a subclass of\n                    <jats:italic>local theories<\/jats:italic>\n                    in which\n                    <jats:italic>partial quantifier elimination<\/jats:italic>\n                    can be performed efficiently. We present\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\mathcal {T}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>T<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -QEL a parametrized polynomial time algorithm that is a sound extension of QEL and is relatively complete for this class of theories. The algorithm utilizes the proof theoretic characterization of the theories, which is based on\n                    <jats:italic>restricted derivations<\/jats:italic>\n                    . Finally, we prove for\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\mathcal {T}$$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mi>T<\/mml:mi>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    -QEL, soundness in general, and relative completeness with respect to the identified class of theories.\n                  <\/jats:p>","DOI":"10.1007\/978-3-031-99984-0_26","type":"book-chapter","created":{"date-parts":[[2025,7,29]],"date-time":"2025-07-29T11:47:53Z","timestamp":1753789673000},"page":"490-507","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Relatively Complete and\u00a0Efficient Partial Quantifier Elimination"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-6912-1558","authenticated-orcid":false,"given":"Estifanos","family":"Getachew","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5964-6792","authenticated-orcid":false,"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-4235-9328","authenticated-orcid":false,"given":"Richard","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,30]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N.S., Janota, M.: Playing with quantified satisfaction. LPAR (short papers) 35, 15\u201327 (2015)","DOI":"10.29007\/vv21"},{"issue":"1\u20132","key":"26_CR2","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"JH Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1\u20132), 29\u201335 (1988)","journal-title":"J. Symb. Comput."},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. LNCS, vol.\u00a08559, pp. 737\u2013744. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49","DOI":"10.1007\/978-3-319-08867-9_49"},{"key":"26_CR4","unstructured":"Dutertre, B.: Solving exists\/forall problems with yices. In: Workshop on Satisfiability Modulo Theories (2015)"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Harcourt\/Academic Press, Burlington, MA, 2nd edn. (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, Second Edition. Graduate Texts in Computer Science, Springer (1996). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"Ganzinger, H.: Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 81\u201390. IEEE (2001)","DOI":"10.1109\/LICS.2001.932485"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"Garcia-Contreras, I., Hari\u00a0Govind, V.K., Shoham, S., Gurfinkel, A.: Fast approximations of quantifier elimination. In: Computer aided verification. Part II, Lecture Notes in Comput. Sci., vol. 13965, pp. 64\u201386. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_4","DOI":"10.1007\/978-3-031-37703-7_4"},{"key":"26_CR9","doi-asserted-by":"publisher","unstructured":"Ghilardi, S., Ranise, S.: MCMT: A model checker modulo theories. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS (LNAI), vol. 6173, pp. 22\u201329. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14203-1_3","DOI":"10.1007\/978-3-642-14203-1_3"},{"issue":"4","key":"26_CR10","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1145\/566385.566387","volume":"3","author":"R Givan","year":"2002","unstructured":"Givan, R., Mcallester, D.: Polynomial-time computation via local inference relations. ACM Trans. Comput. Logic (TOCL) 3(4), 521\u2013541 (2002)","journal-title":"ACM Trans. Comput. Logic (TOCL)"},{"key":"26_CR11","unstructured":"Givan, R., McAllester, D.A.: New results on local inference relations. In: Nebel, B., Rich, C., Swartout, W.R. (eds.) Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR 1992). Cambridge, MA, USA, October 25-29, 1992, pp. 403\u2013412. Morgan Kaufmann (1992)"},{"key":"26_CR12","unstructured":"Haase, C., Krishna, S.N., Madnani, K., Mishra, O.S., Zetzsche, G.: An efficient quantifier elimination procedure for presburger arithmetic. In: Bringmann, K., Grohe, M., Puppis, G., Svensson, O. (eds.) 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, July 8-12, 2024, Tallinn, Estonia. LIPIcs, vol.\u00a0297, pp. 142:1\u2013142:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2024.142"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Hodges, W.: Logical features of Horn clauses. In: Handbook of logic in artificial intelligence and logic programming, vol. 1, pp. 449\u2013503. Oxford Sci. Publ., Oxford Univ. Press, New York (1993)","DOI":"10.1093\/oso\/9780198537458.003.0007"},{"key":"26_CR14","unstructured":"Hodges, W.: Model Theory. Encyclopedia of Mathematics and its Applications 42, Cambridge University Press, 1 edn. (1993)"},{"key":"26_CR15","doi-asserted-by":"publisher","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_2","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"Kroening, D., Strichman, O.: Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-50497-0","DOI":"10.1007\/978-3-662-50497-0"},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: Zorn, B.G., Aiken, A. (eds.) Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, pp. 316\u2013329. ACM (2010). https:\/\/doi.org\/10.1145\/1806596.1806632","DOI":"10.1145\/1806596.1806632"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"McAllester, D.A.: Automatic recognition of tractability in inference relations. J. ACM 40(2), 284\u2013303 (1993). https:\/\/doi.org\/10.1145\/151261.151265","DOI":"10.1145\/151261.151265"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Nelson, G., Oppen, D.C.: Fast decision algorithms based on union and find. In: 18th Annual Symposium on Foundations of Computer Science (Providence, R.I., 1977), pp. 114\u2013119. IEEE, Long Beach, CA (1977)","DOI":"10.1109\/SFCS.1977.12"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. J. ACM 27(3), 403\u2013411 (1980). https:\/\/doi.org\/10.1145\/322203.322204","DOI":"10.1145\/322203.322204"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Riley, D., Fedyukovich, G.: Multi-phase invariant synthesis. In: Roychoudhury, A., Cadar, C., Kim, M. (eds.) Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2022, Singapore, Singapore, November 14-18, 2022, pp. 607\u2013619. ACM (2022). https:\/\/doi.org\/10.1145\/3540250.3549166","DOI":"10.1145\/3540250.3549166"},{"issue":"7","key":"26_CR23","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"RE Shostak","year":"1978","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Commun. ACM 21(7), 583\u2013585 (1978)","journal-title":"Commun. ACM"},{"key":"26_CR24","doi-asserted-by":"publisher","unstructured":"Sofronie-Stokkermans, V.: Hierarchic reasoning in local theory extensions. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 219\u2013234. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_16","DOI":"10.1007\/11532231_16"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 30"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-99984-0_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:27:48Z","timestamp":1781882868000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-99984-0_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031999833","9783031999840"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-99984-0_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"30 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interest"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Stuttgart","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.dhbw-stuttgart.de\/cade-30\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}