Knowledge Representation for Mathematics

数学知识表示

• 批准号: 8819624
• 负责人: David McAllester
• 金额: $ 12.01万
• 依托单位: Massachusetts Institute of Technology
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 1988
• 资助国家: 美国
• 起止时间: 1988-09-01 至 1991-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=8819624&HistoricalAwards=false
• 关键词: Knowledge; Representation; Mathematics

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.

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