Mining counterexamples for wide-signature algebras with an Isabelle server

TL;DR

This paper presents a parallel approach using an Isabelle server and Python client to efficiently find counterexamples in algebraic structures, resolving open questions about identities in residuated binars.

Contribution

It introduces a novel Python-Isabelle framework for counterexample search and demonstrates its effectiveness through computational experiments.

Findings

Counterexamples found for open questions in algebraic identities

Efficient parallel search method implemented with Isabelle

Resolved interdependencies between distributive-like identities

Abstract

We propose an approach for searching for counterexamples of statements about algebraic structures with a medium-sized signature using the Isabelle proof assistant in an efficient, parallel manner. We contribute a Python client Isabelle server and other scripts implementing our approach, and provide results of our computational experiments. In particular, our experiments yield counterexamples that resolve a previously open question regarding the interdependencies between distributive-like identities in residuated binars.