Knowledge Representation for Mathematics

通过对纯数学中已知定理的基础验证，对新的自动定理证明技术进行了检验和评价。研究者已经使用面向对象的推理技术从集合论公理中验证了布尔格的Stone表示定理。新的推理技术是通过测量从根本上验证Bledsoe的十个挑战问题所需的用户给出的细节量来评估的。要评估的推理技术包括新的前向链约束传播技术，用于数学归纳的前向链机制，用于面向对象推理的自动焦点控制，以及用于验证和应用用户定义算法的健全机制。自动推理是人工智能的核心问题之一，在软件和硬件验证、演绎数据检索、在线文档系统以及数学和科学领域的计算机辅助教学中具有潜在的应用前景。本研究旨在证明自动推理可以在实践中使用，并且正在朝着更有效的方法取得进展。

New automatic theorem proving techniques are examined and evalu- ated by foundationally verifying well known theorems in pure mathematics. The investigator has already used object-oriented inference techniques to verify the Stone representation theorem for Boolean lattices from the axioms of set theory. The new inference techniques are evaluated by measuring the amount of user-given detail needed to foundationally verify Bledsoe's ten challenge problems. The inference techniques to be evaluated include new forward chaining constraint propagation techniques, a forward chaining mechanism for mathematical induction, automated focus control for object-oriented inference, and a sound mechan- ism for verifying and applying user-defined algorithms. Automatic reasoning is one of the central problems of artificial intelligence, with potential for application in software and hardware verification, deductive data retrieval, online docu- mentation systems, and computer-aided instruction in mathematics and the sciences. This research seeks to establish that auto- matic inference can be used in practice and that progress is being made toward ever more effective methods.