Leveraging the Information Contained in Theory Presentations
Journal Articles
Overview
Research
Identity
Additional Document Info
View All
Overview
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.
We 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.
