26 citations · 38 across the 5 of their papers we have counts for
5 papers
The Vampire Diary
Filip Bártek, Ahmed Bhayat, Robin Coutelier +10
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…
Superposition with Delayed Unification
Ahmed Bhayat, Johannes Schoisswohl, Michael Rawson
Classically, in saturation-based proof systems, unification has been considered atomic. However, it is also possible to move unification to the calculus level, turning the steps of…
Automating Induction by Reflection
Johannes Schoisswohl, Laura Kovács
Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The rea…
Automating Induction by Reflection
Johannes Schoisswohl, Laura Kovacs
Despite recent advances in automating theorem proving in full first-order theories, inductive reasoning still poses a serious challenge to state-of-the-art theorem provers. The rea…
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…