3 citations · 7 across the 6 of their papers we have counts for
4 papers · 1 filter
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…
Term Ordering Diagrams
Márton Hajdu, Robin Coutelier, Laura Kovács +1
The superposition calculus for reasoning in first-order logic with equality relies on simplification orderings on terms. Modern saturation provers use the Knuth-Bendix order (KBO)…
Lazy Reimplication in Chronological Backtracking
Robin Coutelier, Mathias Fleury, Laura Kovács
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is…
SAT Solving for Variants of First-Order Subsumption
Robin Coutelier, Jakob Rath, Michael Rawson +2
Automated reasoners, such as SAT/SMT solvers and first-order provers, are becoming the backbones of rigorous systems engineering, being used for example in applications of system v…