Pith. sign in

REVIEW 3 major objections 6 minor 71 references

The Vampire Diary

T0 review · 3 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Vampire now proves theorems that combine quantified arithmetic, structural induction, and polymorphic types in one saturation-based proof search.

desk verdict A solid, honest tool paper that consolidates Vampire's new integrated capabilities; the main claim is credible but the SMT comparison and unpublished arithmetic rules deserve a bit more transparency. read the letter →

arxiv 2506.03030 v3 pith:G4KSTLQ5 submitted 2025-06-03 cs.LO

Filip Bártek , Ahmed Bhayat , Robin Coutelier , Márton Hajdu , Matthias Hetzenberger , Petra Hozzová , Laura Kovács , Jakob Rath
show 5 more authors
Michael Rawson Giles Reger Martin Suda Johannes Schoisswohl Andrei Voronkov
This is my paper
classification cs.LO
keywords automatedtheoremprovingsuperpositioncalculusstructuralinductionquantifiedarithmeticrank-1polymorphismSMTintegrationsaturation-basedproofsearchVampire
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This tool paper presents the theorem prover Vampire as it now stands: a single automated reasoning system that handles polymorphic first-order logic with quantifiers, theories such as mixed integer-real arithmetic, and structural induction in the same proof search. The central demonstration is an automatically found proof that the sum of two lists of real numbers equals the sum of their concatenation, a theorem that needs arithmetic, an algebraic datatype, a recursive function, and an inductive step. The paper's claim is that Vampire has reached the point where such verification-style problems can be handed to it directly, complementing SMT solvers and proof assistants. It also serves as a user guide to schedules, options, and reading refutations.

What carries the argument

The load-bearing machinery is a saturation-based superposition calculus whose search state is partitioned into clauses and driven by the AVATAR architecture for splitting, extended in three directions: the ALASCA calculus rewrites equalities modulo linear arithmetic instead of only by syntactic superposition; structural induction is applied as an inference rule that instantiates an induction axiom with the current goal and immediately resolves the generated lemmas; and rank-1 polymorphism lets the same clauses range over lists of any element type. The arithmetic side also includes a conflict-driven quantifier-elimination routine (VIRAS) and, per a footnote, unpublished inference rules for mixed integer-real arithmetic with a floor function, plus optional hand-off of ground arithmetic to an SMT solver.

What would settle it

Feed Vampire an input in the mixed integer-real fragment that uses the floor function and an uninterpreted function, such that the input is actually satisfiable, and observe whether Vampire reports unsatisfiable; alternatively, take the Figure 3 proof, translate each 'Alasca normalization' step into explicit linear-arithmetic consequences, and check whether every step is valid under the standard axioms of the reals and integers.

Watch

Extended reading notes

Core claim

The paper's central claim is that Vampire has become an automated solver for the combined theories of commonly used data structures, and that the combination is now strong enough for practical use: in the flagship demonstration, when given the natural first-order formalization of the sum-of-append problem, the system finds a proof immediately. The proof is produced by interleaving structural induction on lists with ALASCA's superposition-based arithmetic rewriting, under rank-1 polymorphism, and the authors add that other solvers such as CVC5 or Z3 cannot, to their knowledge, yet process or prove such a problem.

Load-bearing premise

The load-bearing premise is that all of Vampire's implemented inference rules are sound together, most importantly the still-unpublished rules for mixed integer-real arithmetic with the floor function; if any rule is wrong, the demonstration proof would not actually prove the theorem.

Editorial extensions

If this is right

  • A user can give Vampire an SMT-LIB problem combining recursive datatypes, quantifiers, and arithmetic and expect a proof or countermodel without manually splitting the problem.
  • Vampire can serve as a complement to SMT solvers by handling the quantified parts that ground SMT approaches struggle with, while offloading ground arithmetic to them.
  • The demonstrated sum-of-concatenation proof suggests that verification obligations about list-processing functions are within reach of a single automated run.
  • The portfolio schedule mechanism lets non-expert users choose a pre-built schedule tuned for theorem proving, SMT-style theory reasoning, or induction.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • A natural next test is to run the motivating sum-of-append problem under current CVC5 and Z3 releases to confirm the stated gap; if either solver now handles it, the demonstration's contrast weakens but the integrated capability claim stands.
  • Because the mixed integer-real inference rules are unpublished, the soundness of proof certificates ultimately rests on code reading; publishing those rules and their soundness proof would let proof checkers trust Vampire's output in this fragment.
  • Extending the one-free-variable induction restriction to multiple induction variables would likely widen the class of verification problems Vampire can close automatically, and the paper's interleaving machinery suggests a path for trying it.
  • The same combination of ALASCA, induction, and polymorphism could be benchmarked against inductive theorem provers on standard list and array benchmarks to map where saturation-based reasoning beats dedicated inductive provers.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. This paper is a system description of the Vampire theorem prover, positioned as a follow-up to the authors' CAV 2013 tutorial. It gives a user guide covering licensing, installation, invocation, output formats, resource limits, and inspection of proof state, and then presents the main new reasoning capabilities: superposition-based linear arithmetic via the ALASCA calculus and unpublished extensions to mixed integer-real arithmetic, structural and well-founded induction schemata embedded in saturation, rank-1 polymorphism, FOOL, higher-order logic, and program synthesis. The paper also describes engineering work in preprocessing, AVATAR and SMT integration, redundancy elimination, and portfolio schedule construction. The central demonstration is an automated proof of the theorem that summing a concatenation of two real lists equals the sum of the sums, formalized in polymorphic first-order logic with algebraic datatypes; Figure 3 gives a distilled refutation that uses structural induction and ALASCA. The authors claim that CVC5 and Z3 cannot, to the best of their knowledge, yet process or prove such problems, and they cite CASC-J12 results as external evidence of Vampire's competitiveness.

Significance. The integrated capability claim is significant: if correct, Vampire currently sits at a point where quantified arithmetic, structural induction, and polymorphism are combined in one saturation-based prover, and the sum/append example is a good stress test of that integration because each ingredient is needed. The paper's strengths include a reusable CAV evaluation artifact, a concrete printed refutation rather than a black-box success claim, and external anchoring in the CASC-J12 results. The printed proof appears internally consistent and relies on the published ALASCA calculus and published induction framework, so I do not see an internal contradiction in the central derivation. The main caveats are that (i) footnote 9 discloses that the mixed integer-real inference rules are unpublished, so the broad advertised theory support lacks an independent soundness statement, and (ii) the comparative claim about CVC5 and Z3 is empirically unsupported, though it is hedged. These caveats do not, in my view, undermine the specific Figure 3 demonstration, but they should be addressed before publication.

major comments (3)
  1. [Section 4.1, footnote 9] The paper advertises native support for mixed integer-real arithmetic with floor-function support, but footnote 9 says the inference system has not been published. This is a missing support for a novel capability claim. Please state precisely which rules are new, which are from reference [56], and what soundness and completeness status is known, or provide a technical report or preprint. It would also help to state explicitly that Figure 3 does not use these rules and therefore the demonstration rests only on published calculi.
  2. [Section 3 and artifact] The central demonstration is not reproducible from the text alone: no Vampire version or commit, exact command or schedule, runtime, or input file is given, and Figure 3 is said to be 'distilled' rather than verbatim output. Since this proof is the only in-paper witness of the integrated capability, please add a short reproducibility subsection or artifact appendix with the precise invocation and a machine-readable TSTP proof, and state whether Figure 3 is actual output or a human-polished rendering.
  3. [Section 3] The sentence about CVC5 and Z3 is a comparative empirical claim. Even with the hedge 'to the best of our knowledge,' it should be backed by a brief description of the attempted inputs and versions and the outcomes, or weakened to a statement such as 'we are not aware of published support for this combination' to avoid an unverifiable claim.
minor comments (6)
  1. [Section 4.2 and Figure 3] The text says clauses 6 and 7 are ¬L[ϵ]∨L[σ4] and ¬L[ϵ]∨¬L[σ3#σ4], but in the figure those clauses appear in the opposite order; please align the numbering or the prose.
  2. [Section 4.2] Since the induction formula contains two Skolem constants, clarify that σ0 is a parameter while induction is on the list argument; the current wording about 'up to one free variable' may confuse readers.
  3. [References] References [51] and [52] are the same paper with the same title and venue; the duplicate should be removed.
  4. [Section 3] The word 'immediately' should be replaced with a measured runtime or a qualitative statement such as 'within a few seconds,' and the Vampire version and schedule used for the demonstration should be named.
  5. [Section 2] The option listing command is written as '--show_options on'; format it as a code snippet with a value, for example 'vampire --show_options on', to avoid confusion with the option name itself.
  6. [Section 4.1] The new mixed-integer rules are referred to as 'various new inference rules' without names; if they cannot be described in detail, at least give a pointer to the relevant code modules in the artifact.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found; the sum/append proof is a genuine derivation and the capability claims are anchored by the open-source artifact and external competition results.

full rationale

This is a system/tool paper rather than a paper deriving a mathematical result from first principles, so the circularity patterns involving fitted inputs or self-definition do not apply. The central demonstration, the sum/append problem in Figure 2, is a concrete first-order problem with explicit axioms; the proof in Figure 3 is a step-by-step refutation derived from those axioms and the negated conjecture, using structural induction and ALASCA superposition. Nothing in the proof is an input disguised as a prediction: the induction axiom is instantiated with the goal's predicate, and the ALASCA steps are rewrites modulo linear arithmetic, each justified by the displayed clauses. The paper's broader capability claims are supported by external evidence, including the CASC-J12 results [64] and the open-source artifact, and by previously published calculi [37, 40, 53] whose correctness is independent of the present demonstration. The many self-citations are appropriate for a "diary" paper describing an evolving system and are not load-bearing reductions to the paper's own conclusions. Footnote 9 discloses that some mixed integer-real arithmetic inference rules are unpublished; this is an honestly stated support gap about artifact soundness, not circularity, because the Figure 3 proof does not rely on those rules and the claim remains externally testable against the open-source code. Therefore no circular step can be exhibited, and the circularity score is 0.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

This is a tool paper, not a theoretical derivation, so the ledger records background results the system's claims lean on rather than fitted constants. There are no free parameters in any stated claim: the schedule tuning in Section 5.4 configures the artifact, and no quantitative result in the paper depends on a fitted value. No new theoretical entities are introduced; the Skolem constants in Figure 3 are ordinary proof artifacts. The main trust assumptions are the soundness of published calculi (superposition, ALASCA, constrained higher-order unification) and, more fragilely, the soundness of the unpublished mixed integer-real inference rules disclosed in footnote 9.

assumptions (6)
  • standard math The superposition calculus is refutationally sound and complete for first-order logic.
    Section 2.1 describes refutation search via superposition and refers the calculus details to [41].
  • standard math ALASCA is sound and complete for quantified linear real arithmetic with uninterpreted functions.
    Section 4.1 builds Vampire's arithmetic reasoning on ALASCA, citing [37].
  • domain assumption Structural induction over inductively defined datatypes, interval induction over integers, and well-founded induction from recursive definitions are sound as inference rules.
    Section 4.2 embeds induction schemata as inference rules; the schemata are standard, but the triggering and lemma-generation strategies are implementation-specific.
  • ad hoc to paper The new mixed integer-real arithmetic inference rules, including floor-function support, are sound.
    Section 4.1, footnote 9, states this inference system has not been published yet; soundness is not independently documented.
  • domain assumption Bounded-depth higher-order unification with constraint introduction is sound.
    Section 4.4 describes the HOL calculus; soundness is cited to the published HOL branch [10].
  • domain assumption External solvers (CaDiCaL, MiniSat for SAT; Z3 for ground theory reasoning) return correct results for delegated subproblems.
    Sections 2 and 5.2 delegate ground reasoning to these solvers, so Vampire's soundness inherits their correctness.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Vampire Diary." pith.science (2026). https://pith.science/paper/G4KSTLQ5

@misc{pith2026250603030,
  author       = {Pith},
  title        = {Pith review of: The Vampire Diary},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/G4KSTLQ5}},
  note         = {Machine review of arXiv:2506.03030}
}
read the original abstract

During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now supports arithmetic, induction, and higher-order logic. These advances have been made to meet the demands of software verification, enabling Vampire to effectively complement SAT/SMT solvers and aid proof assistants. We explain how best to use Vampire in practice and review the main changes Vampire has undergone since its last tool presentation, focusing on the engineering principles and design choices we made during this process.

Figures

Figures reproduced from arXiv: 2506.03030 by the authors.

Figure 1
Figure 1. Vampire timeline since our 2013 tutorial tool paper [41]. Our advances in saturation-based reasoning proved to make a difference. Vampire outperforms or complements many other state-of-the-art reasoners, including leading SMT solvers and inductive theorem provers. For example, in CASC-J12, the most recent world championship in theorem proving, Vampire proved more problems than any other system in every competition d… view at source ↗
Figure 2
Figure 2. Motivating example in polymorphic first-order logic with uninterpreted func￾tions sum : [R] → R, ++ : Λα. [α] × [α] → [α], algebraic datatypes and real arithmetic. The proof displays some new features of Vampire, in particular the use of structural induction (Sect. 4.2) and superposition-based arithmetic reasoning via the ALASCA calculus (Sect. 4.1). These features are key to Vampire’s success on this problem. The n… view at source ↗
Figure 3
Figure 3. Vampire’s proof output of the problem from [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

71 extracted references · 68 canonical work pages

  1. [56]

    In: LPAR

    Schoisswohl, J., Kovács, L., Korovin, K.: VIRAS: Conflict-Driven Quantifier Elim- ination for Integer-Real Arithmetic. In: LPAR. pp. 147–164 (2024)

    work page 2024

  2. [1]

    CoRRabs/2311.07185 (2023)

    Assaf, A., Burel, G., Cauderlier, R., Delahaye, D., Dowek, G., Dubois, C., Gilbert, F., Halmagrand, P., Hermant, O., Saillard, R.: Dedukti: a Logical Framework based on the λΠ-Calculus Modulo Theory. CoRRabs/2311.07185 (2023)

    arXiv 2023

  3. [2]

    In: TACAS

    Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mo- hamed, A., Mohamed, M., Niemetz, A., Nötzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A Versatile and Industrial- Strength SMT Solver. In: TACAS. pp. 415–442 (2022)

    work page 2022

  4. [3]

    www.SMT-LIB.org (2016)

    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)

    work page 2016

  5. [4]

    Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability modulo Theories Competition. In: CAV. p. 20–23 (2005)

    work page 2005

  6. [5]

    In: IJCAR

    Bártek, F., Chvalovský, K., Suda, M.: Regularization in Spider-Style Strategy Dis- covery and Schedule Construction. In: IJCAR. pp. 194–213 (2024)

    work page 2024

  7. [6]

    In: LPAR

    Bhayat, A., Korovin, K., Kovács, L., Schoisswohl, J.: Refining Unification with Abstraction. In: LPAR. pp. 36–47 (2023)

    work page 2023

  8. [7]

    In: IJCAR

    Bhayat, A., Reger, G.: A Combinator-Based Superposition Calculus for Higher- Order Logic. In: IJCAR. pp. 278–296 (2020)

    work page 2020

Show all 71 references
  1. [8]

    In: IJCAR

    Bhayat, A., Reger, G.: A PolymorphicV ampire(Short Paper). In: IJCAR. pp. 361–368 (2020)

    2020

  2. [9]

    In: CADE

    Bhayat, A., Schoisswohl, J., Rawson, M.: Superposition with Delayed Unification. In: CADE. pp. 23–40 (2023)

    2023

  3. [10]

    In: IJCAR

    Bhayat, A., Suda, M.: A Higher-OrderV ampire(Short Paper). In: IJCAR. pp. 75–85 (2024)

    2024

  4. [11]

    Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: Cadical 2.0. In: CAV. pp. 133–152 (2024). https://doi.org/10.1007/978-3-031-65627-9_7, https://doi.org/10.1007/978-3-031-65627-9_7 The V ampireDiary 13

    2024 doi

  5. [12]

    In: CADE

    Blanchette, J.C., Paskevich, A.: TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. In: CADE. pp. 414–420 (2013)

    2013

  6. [13]

    In: CADE (2013)

    Claessen, K., Johansson, M., Rosén, D., Smallbone, N.: Automating Inductive Proofs Using Theory Exploration. In: CADE (2013)

    2013

  7. [14]

    In: WS on Model Computation - Principles, Algorithms and Applications (2003)

    Claessen, K., Sörensson, N.: New Techniques that Improve MACE-style Model Finding. In: WS on Model Computation - Principles, Algorithms and Applications (2003)

    2003

  8. [15]

    Formal Methods in System Design (2024)

    Coutelier, R., Rath, J., Rawson, M., Biere, A., Kovács, L.: SAT Solving for Variants of First-Order Subsumption. Formal Methods in System Design (2024)

    2024

  9. [16]

    In: TACAS

    De Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: TACAS. pp. 337–340 (2008)

    2008

  10. [17]

    Desharnais, M., Vukmirović, P., Blanchette, J., Wenzel, M.: Seventeen Provers Under the Hammer. In: ITP. pp. pp. 8:1–8:18 (2022)

    2022

  11. [18]

    Eén, N., Sörensson, N.: An Extensible SAT-solver. In: SAT. pp. 502–518 (2003)

    2003

  12. [19]

    Graf, P.: Substitution Tree Indexing. In: RTA. pp. 117–131 (1995)

    1995

  13. [20]

    Granlund, T.: The GNU Multiple Precision Arithmetic Library (2023), https:// gmplib.org/gmp-man-6.3.0.pdf

    2023

  14. [21]

    In: CADE (2025), to appear

    Hajdu, M., Coutelier, R., Kovács, L., Voronkov, A.: Term Ordering Diagrams. In: CADE (2025), to appear

    2025

  15. [22]

    In: Principles of Systems Design

    Hajdu, M., Hozzová, P., Kovács, L., Reger, G., Voronkov, A.: Getting Saturated with Induction. In: Principles of Systems Design. pp. 306–322 (2022)

    2022

  16. [23]

    In: CICM

    Hajdu, M., Hozzová, P., Kovács, L., Schoisswohl, J., Voronkov, A.: Induction with Generalization in Superposition Reasoning. In: CICM. pp. 123–137 (2020)

    2020

  17. [24]

    EasyChair Preprint no

    Hajdu, M., Kovacs, L., Rawson, M., Voronkov, A.: TheV ampireApproach to Induction. EasyChair Preprint no. 9217 (EasyChair, 2022)

    2022

  18. [25]

    In: LPAR

    Hajdu, M., Kovács, L., Rawson, M.: Rewriting and Inductive Reasoning. In: LPAR. pp. 278–294 (2024)

    2024

  19. [26]

    In: FMCAD

    Hajdu, M., Hozzová, P., Kovács, L., Voronkov, A.: Induction with Recursive Defi- nitions in Superposition. In: FMCAD. pp. 1–10 (2021)

    2021

  20. [27]

    In: IJCAR

    Hozzová, P., Amrollahi, D., Hajdu, M., Kovács, L., Voronkov, A., Wagner, E.M.: Synthesis of Recursive Programs in Saturation. In: IJCAR. p. 154–171 (2024)

    2024

  21. [28]

    In: CADE

    Hozzová, P., Kovács, L., Norman, C., Voronkov, A.: Program synthesis in satura- tion. In: CADE. pp. 307–324 (2023)

    2023

  22. [29]

    In: CADE

    Hozzová, P., Kovács, L., Voronkov, A.: Integer Induction in Saturation. In: CADE. pp. 361–377 (2021)

    2021

  23. [30]

    International Organi- zation for Standardization, Geneva, Switzerland (Dec 2017)

    ISO: ISO/IEC 14882:2017: Programming languages — C+ +. International Organi- zation for Standardization, Geneva, Switzerland (Dec 2017)

    2017

  24. [31]

    In: TACAS

    Järvisalo, M., Biere, A., Heule, M.: Blocked Clause Elimination. In: TACAS. pp. 129–144 (2010)

    2010

  25. [32]

    Jeanteur, S., Kovács, L., Maffei, M., Rawson, M.: CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model. In: SP. pp. 3165–3183 (2024)

    2024

  26. [33]

    Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Ap- proach, vol. 3. Springer (06 2000). https://doi.org/10.1007/978-1-4615-4449-4

    2000 doi

  27. [34]

    In: LPAR

    Kiesl, B., Suda, M., Seidl, M., Tompits, H., Biere, A.: Blocked Clauses in First- Order Logic. In: LPAR. pp. 31–48 (2017)

    2017

  28. [35]

    Kitware, I.: CMake (2025), https://cmake.org/

    2025

  29. [36]

    In: IJCAR

    Korovin, K.: iProver — An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: IJCAR. pp. 292–298 (2008)

    2008

  30. [37]

    In: TACAS

    Korovin, K., Kovács, L., Reger, G., Schoisswohl, J., Voronkov, A.: ALASCA: Rea- soning in Quantified Linear Arithmetic. In: TACAS. pp. 647–665 (2023) 14 The V ampireTeam

    2023

  31. [38]

    Kotelnikov, E., Kovács, L., Reger, G., Voronkov, A.: TheV ampireand the FOOL. In: CPP. pp. 37–48 (2016)

    2016

  32. [39]

    In: IJCAR

    Kotelnikov, E., Kovács, L., Voronkov, A.: A FOOLish Encoding of the Next State Relations of Imperative Programs. In: IJCAR. pp. 405–421 (2018)

    2018

  33. [40]

    In: IJCAR

    Kovács, L., Hozzová, P., Hajdu, M., Voronkov, A.: Induction in Saturation. In: IJCAR. pp. 21–29 (2024)

    2024

  34. [41]

    Kovács, L., Voronkov, A.: First-Order Theorem Proving andV ampire. In: CAV. pp. 1–35 (2013)

    2013

  35. [42]

    In: Fields of Logic and Computation III

    Lifschitz, V., Lühne, P., Schaub, T.: Towards Verifying Logic Programs in the Input Language of clingo. In: Fields of Logic and Computation III. pp. 190–209 (2020)

    2020

  36. [43]

    Microsoft: Windows Subsystem for Linux (WSL), https://ubuntu.com/desktop/ wsl

  37. [44]

    MIT press (1997)

    Milner, R.: The Definition of Standard ML: Revised. MIT press (1997)

    1997

  38. [45]

    Racine, J.: The Cygwin Tools: a GNU Toolkit for Windows (2000)

    2000

  39. [46]

    In: Handbook of Automated Reasoning, pp

    Ramakrishnan, I.V., Sekar, R., Voronkov, A.: Term Indexing. In: Handbook of Automated Reasoning, pp. 1853–1964. Elsevier and MIT Press (2001)

    2001

  40. [47]

    In: GCAI

    Reger, G., Bjørner, N.S., Suda, M., Voronkov, A.: AVATAR Modulo Theories. In: GCAI. pp. 39–52 (2016)

    2016

  41. [48]

    In: TACAS

    Reger, G., Schoisswohl, J., Voronkov, A.: Making Theory Reasoning Simpler. In: TACAS. pp. 164–180 (2021)

    2021

  42. [49]

    Reger, G., Suda, M., Voronkov, A.: Finding Finite Models in Multi-sorted First- Order Logic. In: SAT. pp. 323–341 (2016)

    2016

  43. [50]

    In: GCAI

    Reger, G., Suda, M., Voronkov, A.: New Techniques in Clausal Form Generation. In: GCAI. pp. 11–23 (2016)

    2016

  44. [52]

    In: TACAS

    Reger, G., Suda, M., Voronkov, A.: Unification with Abstraction and Theory In- stantiation in Saturation-Based Reasoning. In: TACAS. pp. 3–22 (2018)

    2018

  45. [53]

    In: CADE

    Reger, G., Voronkov, A.: Induction in Saturation-Based Proof Search. In: CADE. pp. 477–494 (2019)

    2019

  46. [54]

    Riazanov,A.,Voronkov,A.:PartiallyAdaptiveCodeTrees.In:JELIA.pp.209–223 (2000)

    2000

  47. [55]

    Rungta, N.: A Billion SMT Queries a Day (Invited Paper). In: CAV. pp. 3–18 (2022)

    2022

  48. [57]

    In: CADE

    Schulz, S., Cruanes, S., Vukmirović, P.: Faster, Higher, Stronger: E 2.3. In: CADE. pp. 495–507 (2019)

    2019

  49. [58]

    In: CADE

    Smallbone, N.: Twee: An Equational Theorem Prover. In: CADE. pp. 602–613 (2021)

    2021

  50. [59]

    In: TACAS

    Sonnex, W., Drossopoulou, S., Eisenbach, S.: Zeno: An Automated Prover for Properties of Recursive Data Structures. In: TACAS. pp. 407–421 (2012)

    2012

  51. [60]

    In: IJCAR

    Steen, A., Benzmüller, C.: The Higher-Order Prover Leo-III. In: IJCAR. pp. 108– 116 (2018)

    2018

  52. [61]

    In: IJCAR

    Suda, M.: V ampireGetting Noisy: Will Random Bits Help Conquer Chaos? (Sys- tem Description). In: IJCAR. pp. 659–667 (2022)

    2022

  53. [62]

    AI Magazine37(2), 99–101 (2016)

    Sutcliffe, G.: The CADE ATP System Competition - CASC. AI Magazine37(2), 99–101 (2016)

    2016

  54. [63]

    Logic Journal of the IGPL (2022)

    Sutcliffe, G.: The Logic Languages of the TPTP World. Logic Journal of the IGPL (2022). https://doi.org/10.1093/jigpal/jzac068 The V ampireDiary 15

    2022 doi

  55. [64]

    The European Journal on Artificial Intelligence 0(0), 30504554241305110 (0)

    Sutcliffe, G.: The 12th IJCAR Automated Theorem Proving System Com- petition — CASC-J12. The European Journal on Artificial Intelligence 0(0), 30504554241305110 (0)

  56. [65]

    In: LPAR Workshops (2008)

    Sutcliffe, G.: The SZS Ontologies for Automated Reasoning Software. In: LPAR Workshops (2008)

    2008

  57. [66]

    In: LPAR

    Sutcliffe, G.: The TPTP World — Infrastructure for Automated Reasoning. In: LPAR. pp. 1–12 (2010)

    2010

  58. [67]

    Tunney, J.: Cosmopolitan Libc (2025), https://justine.lol/cosmopolitan/

    2025

  59. [68]

    Voronkov, A.: AVATAR: The Architecture for First-Order Theorem Provers. In: CAV. pp. 696–710 (2014)

    2014

  60. [69]

    org/smart-program/Vampire23/2023-07-05.html#talk:223833

    Voronkov, A.: Spider: Learning in the Sea of Options (2023), https://easychair. org/smart-program/Vampire23/2023-07-05.html#talk:223833

    2023

  61. [70]

    Vukmirovic, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S.: Making Higher-Order Superposition Work. J. Autom. Reason.66(4), 541–564 (2022)

    2022

  62. [71]

    Weber, T., Conchon, S., Déharbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015-2018. J. Satisf. Boolean Model. Comput.11(1), 221–259 (2019), https://doi.org/10.3233/SAT190123

    2019 doi

  63. [72]

    In: CADE

    Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: CADE. pp. 140–145 (2009)

    2009

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.