Knowledge Representation for Mathematics

新的自动定理证明技术进行检查和评估， 通过从根本上验证纯理论中的著名定理， 数学 研究人员已经使用面向对象 验证Stone表示定理的推理技术 从集合论的公理中推导出布尔格。 新 推理技术是通过测量 用户给出的细节需要从根本上验证布莱索的十个 挑战问题。 要评估的推理技术 包括新前向链接约束传播技术， 数学归纳法的正向链接机构、自动化的 面向对象推理的焦点控制，以及声音机制， 验证和应用用户定义的算法。 自动推理是人工智能的核心问题之一 智能，具有应用于软件和 硬件验证，演绎数据检索，在线文档， 智能系统和计算机辅助数学教学 和科学。 这项研究旨在建立自动- 自动推理可以在实践中使用，进步是 正在努力寻找更有效的方法。

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.