Showing cs.LOShow all
2 papers · 1 filter
cs.LO2026
A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning
Can Cebeci, Nikolaj Bjørner, George Candea +1
SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously…
cs.LO2025
Verified and Optimized Implementation of Orthologic Proof Search
Simon Guilloud, Clément Pit-Claudel
We report on the development of an optimized and verified decision procedure for orthologic equalities and inequalities. This decision procedure is quadratic-time and is used as a…