Leveraging the Information Contained in Theory Presentations
Jacques Carette, William M. Farmer, and Yasmine Sharoda
2020
Abstract
A theorem prover without an extensive library is much less useful to
its potential users. Algebra, the study of algebraic structures, is a
core component of such libraries. Algebraic theories also are
themselves structured, the study of which was started as Universal
Algebra. Various constructions (homomorphism, term algebras,
products, etc) and their properties are both universal and
constructive. Thus they are ripe for being automated. Unfortunately,
current practice still requires library builders to write these by
hand. %e first highlight specific redundancies in libraries of
existing systems. Then we describe a framework for generating these
derived concepts from theory definitions. We demonstrate the
usefulness of this framework on a test library of 227 theories.