26 citations · 57 across the 8 of their papers we have counts for
8 papers
Formalizing Graph Trail Properties in Isabelle/HOL
Laura Kovacs, Hanna Lachnitt, Stefan Szeider
We describe a dataset expressing and proving properties of graph trails, using Isabelle/HOL. We formalize the reasoning about strictly increasing and decreasing trails, using weigh…
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (Extended Version)
Giles Reger, Martin Suda, Andrei Voronkov
This paper attempts to address the question of how best to assure the correctness of saturation-based automated theorem provers using our experience developing the theorem prover V…
Coming to Terms with Quantified Reasoning
Laura Kovacs, Simon Robillard, Andrei Voronkov
The theory of finite term algebras provides a natural framework to describe the semantics of functional languages. The ability to efficiently reason about term algebras is essentia…
Selecting the Selection
Giles Reger, Martin Suda, Andrei Voronkov +1
Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implement…
Finding Finite Models in Multi-Sorted First Order Logic
Giles Reger, Martin Suda, Andrei Voronkov
This work extends the existing MACE-style finite model finding approach to multi-sorted first order logic. This existing approach iteratively assumes increasing domain sizes and en…
The Vampire and the FOOL
Evgenii Kotelnikov, Laura Kovács, Giles Reger +1
This paper presents new features recently implemented in the theorem prover Vampire, namely support for first-order logic with a first class boolean sort (FOOL) and polymorphic arr…