3 papers
cs.LO2026
Constraint Learning for Non-confluent Proof Search
Michael Rawson, Clemens Eisenhofer, Laura Kovács
Proof search in non-confluent tableau calculi, such as the connection tableau calculus, suffers from excess backtracking, but simple restrictions on backtracking are incomplete. We…
cs.LO2026
When Agda met Vampire
Artjoms Å inkarovs, Michael Rawson
Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in…
cs.LO2024
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…