8 citations · 8 across the 5 of their papers we have counts for
Showing 2026 · cs.LOShow all
2 papers · 2 filters
cs.LO2026
Teaching Vampire New Tricks: An Experimental Study of Neural Clause Selection
Karel Chvalovský, Martin Suda, Josef Urban
A neural clause-selection guidance approach in the Vampire theorem prover was recently shown to substantially improve the success rate of the prover's default strategy on the TPTP…
cs.LO2026
Revisiting Incremental Linearization for Nonlinear Integer Arithmetic
Marek Dančo, Karel Chvalovský, Mikoláš Janota
Incremental Linearization has previously been proposed for solving SMT problems over quantifier-free nonlinear integer arithmetic and has proven effective despite its conceptual si…