• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文学位 >Enhancing the Nuprl proof development system and applying it to computational abstract algebra.
【24h】

Enhancing the Nuprl proof development system and applying it to computational abstract algebra.

机译：增强Nuprl证明开发系统并将其应用于计算抽象代数。

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This thesis describes substantial enhancements that were made to the software tools in the Nuprl system that are used to interactively guide the production of formal proofs. Over 20,000 lines of code were written for these tools. Also, a corpus of formal mathematics was created that consists of roughly 500 definitions and 1300 theorems. Much of this material is of a foundational nature and supports all current work in Nuprl. This thesis concentrates on describing the half of this corpus that is concerned with abstract algebra and that covers topics central to the mathematics of the computations carried out by computer algebra systems.; The new proof tools include those that solve linear arithmetic problems, those that apply the properties of order relations, those that carry out inductive proof to support recursive definitions, and those that do sophisticated rewriting. The rewrite tools allow rewriting with relations of differing strengths and take care of selecting and applying appropriate congruence lemmas automatically. The rewrite relations can be order relations as well as equivalence relations. If they are order relations, appropriate monotonicity lemmas are selected.; These proof tools were heavily used throughout the work on computational algebra. Many examples are given that illustrate their operation and demonstrate their effectiveness.; The foundation for algebra introduced classes of monoids, groups, rings and modules, and included theories of order relations and permutations. Work on finite sets and multisets illustrates how a quotienting operation hides details of datatypes when reasoning about functional programs. Theories of summation operators were developed that drew indices from integer ranges, lists and multisets, and that summed over all the classes mentioned above. Elementary factorization theory was developed that characterized when cancellation monoids are factorial. An abstract data type for the operations of multivariate polynomial arithmetic was defined, and the correctness of an implementation of these operations was verified. The implementation is similar to those found in current computer algebra systems. This work was all done in Nuprl's constructive type theory. The thesis discusses the appropriateness of this foundation, and the extent to which the work relied on it.
机译：本文描述了对Nuprl系统中的软件工具的实质性增强，这些交互用于指导形式证明的产生。为这些工具编写了超过20,000行代码。此外，还创建了一个正式的数学语料库，它由大约500个定义和1300个定理组成。这些材料大部分都是基础材料，支持Nuprl当前的所有工作。本文的重点是描述该语料库中与抽象代数有关的一半，并涵盖了计算机代数系统所进行的计算数学的核心主题。新的证明工具包括解决线性算术问题的工具，应用顺序关系属性的工具，执行归纳证明以支持递归定义的工具以及进行复杂重写的工具。重写工具允许使用不同强度的关系进行重写，并自动选择和应用适当的一致性引理。重写关系可以是顺序关系也可以是等价关系。如果它们是顺序关系，则选择适当的单调引理。这些证明工具在计算代数的整个工作中被大量使用。给出了许多例子来说明其操作并证明其有效性。代数的基础介绍了类曲面，组，环和模块的类，并包括顺序关系和置换的理论。有限集和多集上的工作说明了在对功能程序进行推理时，商操作如何隐藏数据类型的详细信息。求和运算符的理论得到发展，它们从整数范围，列表和多集中提取索引，并且对上述所有类进行求和。提出了基本分解理论，该理论表征了何时消除半定式为阶乘。定义了用于多元多项式算术运算的抽象数据类型，并验证了这些运算实现的正确性。该实现与当前计算机代数系统中的实现类似。这项工作都是在Nuprl的构造型理论中完成的。本文讨论了该基础的适用性，以及在何种程度上依靠该基础。

著录项

  • 作者

    Jackson, Paul Bernard.;

  • 作者单位

    Cornell University.;

  • 授予单位 Cornell University.;
  • 学科 Computer Science.
  • 学位 Ph.D.
  • 年度 1995
  • 页码 279 p.
  • 总页数 279
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类 自动化技术、计算机技术;
  • 关键词

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号