8 citations · 9 across the 5 of their papers we have counts for
5 papers
Reintroducing the Second Player in EPR
Leroy Chew, Mikoláš Janota, Miroslav Olšák +1
We present a PSPACE-complete fragment of first order logic we call QEALM (QBF-like EPR by Alternating Level-ordered Miniscoping). Unlike other well-known fragments it is closer to…
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…
Efficient Neural Clause-Selection Reinforcement
Martin Suda
Clause selection is arguably the most important choice point in saturation-based theorem proving. Framing it as a reinforcement learning (RL) task is a way to challenge the human-d…
A Higher-Order Vampire (Short Paper)
Ahmed Bhayat, Martin Suda
The support for higher-order reasoning in the Vampire theorem prover has recently been completely reworked. This rework consists of new theoretical ideas, a new implementation, and…
Regularization in Spider-Style Strategy Discovery and Schedule Construction
Filip Bártek, Karel Chvalovský, Martin Suda
To achieve the best performance, automatic theorem provers often rely on schedules of diverse proving strategies to be tried out (either sequentially or in parallel) on a given pro…