A Rational Reconstruction of a System for Experimental Mathematics

Jacques Carette, William M. Farmer, and Volker Sorge

2007

Abstract

In previous papers we described the implementation of a system which
combines mathematical object generation, transformation and filtering,
conjecture generation, proving and disproving for mathematical
discovery in non-associative algebra.  While the system has generated
novel, fully verified theorems, their construction involved a lot of
ad hoc communication between disparate systems.  In this paper we
carefully reconstruct a specification of a sub-process of the original
system in a framework for trustable communication between mathematics
systems put forth by us. It employs the concept of biform theories
that enables the combined formalisation of the axiomatic and
algorithmic theories behind the generation process.  This allows us to
gain a much better understanding of the original system, and exposes
clear generalisation opportunities.