Leveraging the Information Contained in Theory Presentations
Jacques Carette, William M. Farmer, Yasmine Sharoda

TL;DR
This paper introduces a framework to automate the generation of algebraic structures and their properties from theory definitions, reducing redundancies in theorem prover libraries and enhancing their utility.
Contribution
It presents a novel automated approach for deriving algebraic concepts from theories, streamlining library construction in theorem proving systems.
Findings
Successfully applied to a library of 227 theories
Reduced manual effort in library development
Improved consistency and completeness of algebraic libraries
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · Advanced Database Systems and Queries
