collaborators

1 paper

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,…