3 citations · 4 across the 3 of their papers we have counts for
3 papers
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…
PolySAT: Word-level Bit-vector Reasoning in Z3
Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann +2
PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-d…
SAT-Based Subsumption Resolution
Robin Coutelier, Laura Kovács, Michael Rawson +1
Subsumption resolution is an expensive but highly effective simplifying inference for first-order saturation theorem provers. We present a new SAT-based reasoning technique for sub…