1 citations · 1 across the 2 of their papers we have counts for
2 papers
cs.LO2026
Case Study: Saturations as Explicit Models in Equational Theories
Mikoláš Janota, Michael Rawson, Stephan Schulz
Automated theorem provers (ATPs) can disprove conjectures by saturating a set of clauses, but the resulting saturated sets are opaque certificates. In the unit equational fragment,…
cs.LO2025★ 1 cited
Case Study: Verified Vampire Proofs in the LambdaPi-calculus Modulo
Anja Petković Komel, Michael Rawson, Martin Suda
The Vampire automated theorem prover is extended to output machine-checkable proofs in the Dedukti concrete syntax for the LambdaPi-calculus modulo. This significantly reduces the…