Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Case Study: Saturations as Explicit Models in Equational Theories

Mikoláš Janota, Michael Rawson, Stephan Schulz

Abstract

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.

Case Study: Saturations as Explicit Models in Equational Theories

Abstract

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.
Paper Structure (9 sections, 7 equations, 1 figure)

This paper contains 9 sections, 7 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Constructing Explicit Models
  4. Case Study: Countermodels of Equational Theories
  5. Checked Models
  6. Related Work
  7. Summary and Future Work
  9. No finite counterexample to $\mathtt{118} \implies \mathtt{274}$

Figures (1)

  • Figure 1: Confluent and terminating system for $118\land \lnot 274$

Theorems & Definitions (3)

  • definition 1: rewrite
  • definition 2: normalisation
  • proof