{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,8]],"date-time":"2026-07-08T22:31:03Z","timestamp":1783549863155,"version":"3.55.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030720124","type":"print"},{"value":"9783030720131","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Reasoning with quantifiers and theories is at the core of many applications in program analysis and verification. Whilst the problem is undecidable in general and hard in practice, we have been making large pragmatic steps forward. Our previous work proposed an instantiation rule for theory reasoning that produced pragmatically useful instances. Whilst this led to an increase in performance, it had its limitations as the rule produces ground instances which (i) can be overly specific, thus not useful in proof search, and (ii) contribute to the already problematic search space explosion as many new instances are introduced. This paper begins by introducing that specifically addresses these two concerns as it produces general solutions and it is a simplification rule, i.e. it replaces an existing clause by a \u2018simpler\u2019 one. Encouraged by initial success with this new rule, we performed an experiment to identify further common cases where the complex structure of theory terms blocked existing methods. This resulted in four further simplification rules for theory reasoning. The resulting extensions are implemented in the <jats:sc>Vampire<\/jats:sc> theorem prover and evaluated on SMT-LIB, showing that the new extensions result in a considerable increase in the number of problems solved, including 90 problems unsolved by state-of-the-art SMT solvers.<\/jats:p>","DOI":"10.1007\/978-3-030-72013-1_9","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:03:10Z","timestamp":1616436190000},"page":"164-180","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Making Theory Reasoning Simpler"],"prefix":"10.1007","author":[{"given":"Giles","family":"Reger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Johannes","family":"Schoisswohl","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Voronkov","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"9_CR1","unstructured":"Vampire website. https:\/\/vprover.github.io\/."},{"key":"9_CR2","unstructured":"E. Althaus, E. Kruglov, and C. Weidenbach. Superposition modulo linear arithmetic SUP(LA). In Frontiers of Combining Systems, 7th International Symposium, FroCoS 2009, Trento, Italy, September 16\u201318, 2009. Proceedings, vol. 5749 of Lecture Notes in Computer Science, pp. 84\u201399. Springer, 2009."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"L. Bachmair, H. Ganzinger, and U. Waldmann. Refutational theorem proving for hierarchic first-order theories. Appl. Algebra Eng. Commun. Comput., 5:193\u2013212, 1994.","DOI":"10.1007\/BF01190829"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"C. Barrett, C. Conway, M. Deters, L. Hadarean, D. Jovanovic, T. King, A. Reynolds, and C. Tinelli. CVC4. In Proceedings of the 23rd International Conference on Computer Aided Verification, number 6806 in Lecture Notes in Computer Science, pp. 171\u2013177. Springer-Verlag, 2011.","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Waldmann. Hierarchic Superposition With Weak Abstraction. In Proceedings of the 24th International Conference on Automated Deduction, number 7898 in Lecture Notes in Artificial Intelligence, pp. 39\u201357. Springer-Verlag, 2013.","DOI":"10.1007\/978-3-642-38574-2_3"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"M. P. Bonacina, C. Lynch, and L. M. de Moura. On deciding satisfiability by theorem proving with speculative inferences. J. Autom. Reasoning, 47(2), 161\u2013189, 2011.","DOI":"10.1007\/s10817-010-9213-y"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"L. M. de Moura and N. Bj\u00f8rner. Z3: an efficient SMT solver. In Proc. of TACAS, vol. 4963 of LNCS, pp. 337\u2013340, 2008.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"N. Dershowitz and D. A. Plaisted. Rewriting. In Handbook of Automated Reasoning, vol. I, chapter 9, pp. 535\u2013610. Elsevier Science, 2001.","DOI":"10.1016\/B978-044450813-3\/50011-4"},{"key":"9_CR9","unstructured":"H. Ganzinger and K. Korovin. Theory instantiation. In Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13\u201317, 2006, Proceedings, vol. 4246 of Lecture Notes in Computer Science, pp. 497\u2013511. Springer, 2006."},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"B. Gleiss and M. Suda. Layered clause selection for theory reasoning. In Automated Reasoning, pp. 402\u2013409. Springer International Publishing, 2020.","DOI":"10.1007\/978-3-030-51074-9_23"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"K. Hoder, G. Reger, M. Suda, and A. Voronkov. Selecting the selection. In Automated Reasoning: 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings, pp. 313\u2013329. Springer International Publishing, 2016.","DOI":"10.1007\/978-3-319-40229-1_22"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"D. Knuth and P. Bendix. Simple word problems in universal algebra. In Computational Problems in Abstract Algebra, pp. 263\u2013297. Pergamon Press, 1970.","DOI":"10.1016\/B978-0-08-012975-4.50028-X"},{"key":"9_CR13","unstructured":"K. Korovin and A. Voronkov. Integrating linear arithmetic into superposition calculus. In Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11\u201315, 2007, Proceedings, vol. 4646 of Lecture Notes in Computer Science, pp. 223\u2013237. Springer, 2007."},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"L. Kov\u00e1cs and A. Voronkov. First-order theorem proving and Vampire. In CAV 2013, vol. 8044 of Lecture Notes in Computer Science, pp. 1\u201335, 2013.","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"A. Nonnengart and C. Weidenbach. Computing small clause normal forms. In Handbook of Automated Reasoning (in 2 volumes), pp. 335\u2013367. Elsevier and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50008-4"},{"key":"9_CR16","unstructured":"G. Reger, N. Bj\u00f8rner, M. Suda, and A. Voronkov. AVATAR modulo theories. In GCAI 2016. 2nd Global Conference on Artificial Intelligence, vol. 41 of EPiC Series in Computing, pp. 39\u201352. EasyChair, 2016."},{"key":"9_CR17","unstructured":"G. Reger and M. Suda. Set of support for theory reasoning. In IWIL Workshop and LPAR Short Presentations, vol. 1 of Kalpa Publications in Computing, pp. 124\u2013134. EasyChair, 2017."},{"key":"9_CR18","unstructured":"G. Reger, M. Suda, and A. Voronkov. The challenges of evaluating a new feature in Vampire. In Proceedings of the 1st and 2nd Vampire Workshops, vol. 38 of EPiC Series in Computing, pp. 70\u201374. EasyChair, 2016."},{"key":"9_CR19","unstructured":"G. Reger, M. Suda, and A. Voronkov. New techniques in clausal form generation. In GCAI 2016. 2nd Global Conference on Artificial Intelligence, vol. 41 of EPiC Series in Computing, pp. 11\u201323. EasyChair, 2016."},{"key":"9_CR20","doi-asserted-by":"crossref","unstructured":"G. Reger, M. Suda, and A. Voronkov. Unification with abstraction and theory instantiation in saturation-based reasoning. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 3\u201322. Springer, 2018.","DOI":"10.29007\/hsh2"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"P. R\u00fcmmer. A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. In Proceedings of the 15th International Conference on Logic for Programming Artificial Intelligence and Reasoning, number 5330 in Lecture Notes in Artificial Intelligence, pp. 274\u2013289. Springer-Verlag, 2008.","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"9_CR22","doi-asserted-by":"crossref","unstructured":"T. Weber, S. Conchon, D. D\u00e9harbe, M. Heizmann, A. Niemetz, and G. Reger. The smt competition 2015\u20132018. Journal on Satisfiability, Boolean Modeling and Computation, 11(1), 221\u2013259, 2019.","DOI":"10.3233\/SAT190123"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-72013-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T18:12:44Z","timestamp":1616436764000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-72013-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030720124","9783030720131"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-72013-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"141","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"29% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}