3 citations · 5 across the 7 of their papers we have counts for
8 papers
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…
Expressive Power of Temporal Message Passing
Przemysław Andrzej Wałęga, Michael Rawson
Graph neural networks (GNNs) have recently been adapted to temporal settings, often employing temporal versions of the message-passing mechanism known from GNNs. We divide temporal…
Scaling CheckMate for Game-Theoretic Security
Sophie Rain, Lea Salome Brugger, Anja Petkovic Komel +2
We present the CheckMate tool for automated verification of game-theoretic security properties, with application to blockchain protocols. CheckMate applies automated reasoning tech…
Rewriting and Inductive Reasoning
Márton Hajdu, Laura Kovács, Michael Rawson
Rewriting techniques based on reduction orderings generate "just enough" consequences to retain first-order completeness. This is ideal for superposition-based first-order theorem…
Spanning Matrices via Satisfiability Solving
Clemens Eisenhofer, Michael Rawson, Laura Kovács
We propose a new encoding of the first-order connection method as a Boolean satisfiability problem. The encoding eschews tree-like presentations of the connection method in favour…
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…