利用理论演示中包含的信息
Leveraging the Information Contained in Theory Presentations
摘要：
一个没有广泛库的定理证明器对它的潜在用户来说用处要小得多。代数，研究代数结构，是这种库的核心组成部分。代数理论本身也是结构化的，对它的研究始于《泛代数》。各种构造（同态、项代数、积等）及其性质都是泛在的和构造性的。因此，它们自动化的时机已经成熟。不幸的是，目前的实践仍然要求库构建者手工编写这些代码。我们首先强调现有系统库中的特定冗余。然后，我们描述了一个框架，从理论定义产生这些派生的概念。我们证明了这个框架的有用性的测试库的227理论。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
