8 citations · 10 across the 4 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2025★ 1 cited
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…
cs.LO2024★ 8 cited
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…