Effective Higher-Order Automated Theorem Proving

有效的高阶自动定理证明

• 批准号: 241609402
• 负责人: Professor Dr.-Ing. Christoph Benzmüller
• 金额: --
• 依托单位: Lehrstuhl für KI-Systementwicklung
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2014
• 资助国家: 德国
• 起止时间: 2013-12-31 至 2017-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/241609402?language=en
• 关键词: Effective; Higher; Order; Automated; Theorem

The automated theorem proving systems LEO-I and LEO-II have found international acclaim as very successful reasoners for classical higher-order logic. Novel contributions of LEO-I include a native (versus axiomatic) treatment of the extensionality principles and the cooperation with external reasoners (such as the first-order prover E) via a flexible agent architecture. The implementation of LEO-II did significantly influence the parallel development of the new higher-order TPTP THF infrastructure for typed higher-order logics, which in turn has led to major system improvements (e.g. in the automated theorem provers ISABELLE/HOL and TPS) and to new systems developments (such as Satallax) for classical higher-order logic. LEO-II has won the international CASC competition in 2010 and it is currently being integrated in the interactive proof assistant ISABELLE/HOL.In this project, we want to turn LEO-II into a theorem prover based on ordered paramodulation/ superposition.These modifications to LEO-II are significant both in theory and practice. The resulting system, called LEO-III, will put an emphasis on ease of integration with other systems.

自动定理证明系统LEO-I和LEO-II作为经典高阶逻辑的非常成功的推理机在国际上受到好评。新的贡献LEO-I包括一个本地（相对于公理）治疗的可拓性原则和合作与外部推理（如一阶证明E）通过一个灵活的代理架构。LEO-II的实现确实显着影响了类型化高阶逻辑的新高阶TPTP THF基础设施的并行开发，这反过来又导致了重大的系统改进（例如自动定理证明器ISABELLE/HOL和TPS）和经典高阶逻辑的新系统开发（例如Satallax）。LEO-II在2010年国际CASC竞赛中获胜，目前正在集成到交互式证明助手ISABELLE/HOL中，本项目希望将LEO-II改造成一个基于有序调制/叠加的定理证明器，这些改进在理论和实践上都具有重要意义。由此产生的系统被称为LEO-III，将强调与其他系统整合的便利性。

项目成果

Going Polymorphic - TH1 Reasoning for Leo-III

走向多态——Leo-III 的 TH1 推理

• DOI: 10.29007/jgkw
• 发表时间: 2017
• 作者: A. Steen;M. Wisniewski;C. Benzmüller
• 通讯作者: C. Benzmüller

There Is No Best \beta -Normalization Strategy for Higher-Order Reasoners

高阶推理机不存在最佳的 β 标准化策略

• DOI: 10.1007/978-3-662-48899-7_23
• 发表时间: 2015
• 作者: A. Steen;C. Benzmüller
• 通讯作者: C. Benzmüller

Effective Normalization Techniques for HOL

HOL 的有效标准化技术

• DOI: 10.1007/978-3-319-40229-1_25
• 发表时间: 2016
• 作者: M. Wisniewski;A. Steen;K. Kern;C. Benzmüller
• 通讯作者: C. Benzmüller

Theorem Provers For Every Normal Modal Logic

每个正规模态逻辑的定理证明

• DOI: 10.29007/jsb9
• 发表时间: 2017
• 作者: T. Gleißner;A. Steen;C. Benzmüller
• 通讯作者: C. Benzmüller