论文标题
利用理论演示中包含的信息
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.
