Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning

Giles Reger, Andrei Voronkov, Martin Suda

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

110 Downloads (Pure)


Reasoning with quantifiers and theories is a very hard problem in program analysis. This paper makes a new contribution to the field by providing a new method of using SMT solvers in saturation-based reasoning. Two new inference rules are introduced for reasoning with non-ground clauses, complementing our recent work on AVATAR modulo theories for ground theory reasoning. The first new rule utilises theory constraint solving (an SMT solver) to perform reasoning within a clause to find an instance where we can remove one or more theory literals. This utilises the power of SMT solvers for theory reasoning with non-ground clauses,reasoning which is currently achieved by the addition of often prolific theory axioms. The second new rule is unification with abstraction where the notion of unification is extended to introduce constraints where theory terms may not otherwise unify. This abstraction is performed lazily, as needed, to allow the superposition theorem prover to make as much progress as possible without the search space growing too quickly. Additionally, the first rule can be used to discharge the constraints introduced by the second. These rules were implemented within the Vampire theorem prover and experimental results show that they are useful for solving a considerable number of previously unsolved problems. The current implementation focuses on complete theories, in particular various versions of arithmetic.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Proceedings
EditorsDirk Beyer, Marieke Huisman
PublisherSpringer Nature
Number of pages20
ISBN (Print)9783319899596
Publication statusPublished - 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10805 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Dive into the research topics of 'Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning'. Together they form a unique fingerprint.

Cite this