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, a saturated set can in fact be read as a convergent rewrite system defining an explicit, possibly infinite, model -- but this is not widely known, even amongst frequent users of ATPs. Moreover, ATPs do not emit these explicit certificates for infinite (counter-)models. We present such a certificate construction in full, implement it in Vampire and E, and apply it to the recent Equational Theories Project, where hundreds of implications do not admit finite countermodels. The resulting rewrite systems can be checked for confluence and termination by existing certified tools, yielding trustworthy countermodels.

翻译：自动定理证明器（ATPs）可以通过子句集的饱和来反驳猜想，但由此产生的饱和集是不透明的证明证书。在单位等式片段中，一个饱和集实际上可以被解读为一个收敛的重写系统，它定义了一个显式的、可能是无限的模型——但这一点即使是在ATPs的频繁用户中也并不广为人知。此外，ATPs不会为无限（反）模型输出这些显式证书。我们完整地提出了这样一种证书构造方法，并在Vampire和E中实现了它，并将其应用于近期的等式理论项目，该项目中有数百个蕴含式不承认有限反模型。由此产生的重写系统可以通过现有的经过认证的工具检查其合流性和终止性，从而得到可信赖的反模型。