1 citations · 1 across the 2 of their papers we have counts for
3 papers · 1 filter
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…
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…
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…