教堂的理论（完结）

叠加计算：Bentkamp等人。 2018年，Bentkamp等人。 2021，Bentkamp等人。 2023a，c

基于组合者的叠加计算：Bhayat＆Reger 2020

4.2验证助理

用于证明教会类型理论（或其扩展）的早期计算机系统包括HOL（Gordon 1988; Gordon＆Melham 1993），TPS（Andrews等，1996; Andrews＆Brown 2006），伊莎贝尔（PVS（沃尔逊1988,1990），PVS（1996年; Shankar 2001），Imms（Farmer等，1993），Hol Light（哈里森1996），Omega（Siekmann等，2006），λClam（Richardson等人1998）。 支持更强大的依赖类型理论的突出验证助理包括COQ（Bertot＆Castéran2004）和最近的精益系统（de moura和Ullrich 2021）。 请参阅下面的其他Internet参考文章，以便链接到以下这些和其他普通普通的其他信息。

上面提到的大多数早期系统集中在互动证明上（至少最初）。 然而，TPS项目特别是自20世纪80年代中期以来一直在工作，以便使用配合方法的ND样式交互式证明和自动定理的集成，并在两者之间进行了调查的防范技术。 该研究在20世纪90年代进一步加剧，当使用所谓的锤子工具，其他项目调查了各种解决方案，例如证明规划和桥梁，如外科定理普通的方法。 当时开发的锤子是今天的早期前体，这是一个非常成功的锤子工具，如大锤，霍比姆和相关系统（Blanchette等，2013，Kaliszyk＆Urban 2015和Czaika＆Kaliszyk 2018）。

虽然由提到的动态引发，但在80年代后期和90年代在教会类型理论的自动化期间，在90年代中提出了一些第一个初步进展，例如，当时的资源投资和成就缺乏如此，例如，在一阶定理证明。 仅在后来培养了良好的进展，特别是通过开发教会类型理论的常用语法，称为TPTP THF（SUTCLIFFE＆BENZMÜLLER2010，SUTCLIFFE 2022）和纳入，从2009年开始，在年度赌场比赛中的TPTP THF师（种类自动定理的世界锦标赛;有关详细信息，请参阅Sutcliffe 2016）。 这些比赛与进一步的因素相结合，引发了对教会类型理论的完全自动化的兴趣。 最近，特别是探讨了使用叠加方法的平等基础定理的探索和SMT技术对HOL的改编。

4.3自动定理普通

提出了一个关于教会类型理论的定理普通的胜利。 重点是过去已成功参与TPTP THF CASC竞赛的系统，并且呈现的顺序是通过他们的首次赌场参与的动机。 最新版本的最新版本可以通过SystemontptP基础架构在线访问（Sutcliffe 2017）。 几乎所有提到的系统都在TPTP TSTP语法中生成可验证的证明证书。

TPS先词（Andrews等，1996年，Andrews＆Brown 2006）可用于自动，交互或半自动地自动地证明基本类型理论或延伸类型理论的定理。 在自动搜索证明时，TPS首先搜索定理的扩展证明（Miller 1987）或展开扩展证明（Brown 2004,2007）。 这一过程的一部分涉及寻找可接受的聚类（Andrews 1981，1999年主教）。 TPS的行为由一组标志控制，也称为模式。 在最新版本的TPS中采用简单的调度机制，以便在有限的时间内顺序地运行大约五十个模式。 TPS是2009年第一届THF赌场比赛的获胜者。

Leo-II箴言（Benzmüller等，2015）是Leo的继任者（Benzmüller＆Kohlhase 1998b，它与Omega校样助手硬连线（Leo代表逻辑引擎欧米茄）。普通普通基于Benzmüller1999a，b的Rue分辨率计算。Leo是第一批实施扩展性的微积分规则，以避免切割模拟效果。Leo-II继承并互补，并提供用于描述和选择的额外微积分规则。通过一阶普通（优选E）和SAT求解器内部合作的先驱具有良好的合作高阶/一阶的防范自动化。由于该箴言往往太弱，无法找到驳斥Leo-II的一些条款在稳步增长的条款中，Leo-II的一些条款获得了特殊状态：它们是一阶条文模制适当的转换功能的应用。因此，Leo-II逐步推出时间有限的呼叫这些条款到一阶定理箴言，以及当一阶箴言报告驳斥时，Leo-II也终止。 这些想法的一部分已经在前任狮子座中实施。 Leo-II与合作一阶定理普通的通信使用TPTP语言和标准。 Leo-II是2010年第二次THF CASC比赛的获胜者。

Satallax Prover（Brown 2012）基于一个完整的教堂类型理论的地面结石，选择（背部和棕色2011）。 初始Tableau分支由猜想和否定结论的假设形成。 从那一点开始，萨塔克斯试图确定该分支的不可起作用或可靠性。 Satallax逐渐产生高阶公式和相应的命题条款。 Satallax使用SAT Solver MiniAT作为发动机，以测试目前的命题条款组的不可起作用。 如果条款不可挑离，原始分支是不可挑离的。 Satallax提供扩展性，描述和选择的微积分规则。 如果功能类型中没有量子，则可以终止更高阶公式和相应的子句。 在这种情况下，如果MiniSAT报告最终的条款集，那么原始的高阶公式组是满足的（通过将所有类型被解释为有限集的标准模型）是满意的。 Satallax是2011年THF Casc竞赛的获胜者，从2013年到2019年

Isabelle / Hol系统（Nipkow，Wenzel和Paulson 2002）最初设计为互动式证明。 但是，为了缓解用户互动，多年来已经增加了几种自动证明策略。 通过适当安排这些证明策略的子集，其中一些非常强大，ISAbelle / HOL已经开始到TPTP THF（以及其他TPTP语法格式）的自动定论者报告，可以从命令运行贝壳像其他普通人一样。 由伊莎贝尔/霍尔计划的最强大的证据策略包括大锤（Blanchette等，2013），它调用了一系列外部一阶和高阶定理普通，模型Finder Nitpick（Blanchette＆nipkow 2010），等级推理SIMP，无型Tableau Prover Blast，简单和古典推理师Auto，Force，Fast，以及最好的第一搜索程序。 与上述所有其他自动定理普通普通相比，Isabelle / HOL的TPTP化身不会输出证明证书。 Isabelle / Hol是2012年THF CASC比赛的获胜者。

Agsyhol先驱基于通用怠速缩小证明搜索算法。 采用回溯，维护相对的搜索状态。 箴言输出证明术语，可以在AGDA系统中验证。

CoQATP实施（非归纳）结构的结构（Bertot＆Castéran2004）。 系统输出证明术语被COQ验证助理所接受作为证明（添加少数定义）。 该箴言使用公理，用于功能扩展性，选择和排除在外。 不支持布尔的扩展性。 除了公理之外，还采用了一个小型基本lemmas的小库。

Leo-III证明者为教会类型理论实施了发道微积分（Steen 2018）。 该系统是Leo和Leo-II的后代，提供了扩展性，描述和选择的微积分规则。 该系统强调了在简化例程和启发式重写方面的有效底层数据结构的实现。 在其前辈的传统中，Leo-III使用翻译为多排序的一阶逻辑配合一阶推理工具。 该证报接受每个常见的TPTP语法方言，因此非常广泛适用。 最近，箴言也延长了几乎每个正常高阶模态逻辑的本地支持（Steen等，2023）。

CVC4，CVC5和Verit（Barbosa等，2019）是基于SMT的自动化普通，用于许多理论，包括线性算术，阵列，位向量，数据类型，有限组和字符串。 这些普通的销售人员已经扩大到教会类型理论的支持（碎片）。

ZipperPosition先驱（Bentkamp等，2018年，Vukmirović等，2022）侧重于教会类型理论的叠加计算的有效实施。 它附带LogTK，用于操纵术语类型理论的术语，公式，条款等的支持库，支持数据类型，递归函数和算术等相关扩展。 ZipperPosition是2020,2021和2022年THF Casc竞赛的获胜者。

Vampire（Bhayat＆Reger 2020）在一阶逻辑中占据了TPTP比赛，现在还支持使用基于组合者的叠加微积分来支持教堂类型理论的自动化。 吸血鬼是2023年THF CASC比赛的获胜者。

定理箴言E（Vukmirović等，2023），另一种突出和主要的一阶级自动定理先词，该秘诀已经延长了教堂的类型理论，使用ZipperPosition的贵屏方法的变种。

Lash（Brown和Kaliszyk 2022）是教会类型理论的定理箴言，被创造为萨拉克斯叉。

Duper是一种基于依赖类型理论的基于叠加的定理箴言，辩称证明了证明助剂的定理。

近年来，从一流到高阶自动定理证明，从一流方面取得了重大转变。

4.4（反击）模型发现

基于Tableau的箴言热（Konrad 1998），已经实施了寻找教会类型理论公式的有限模型或反模型的支持。 限制（反击）模型寻找能力也在普通的Satallax，Leo-II和Leo-III中实施。 目前在系统Nitpick，Nunchaku和反驳中实现了最先进的（有限）模型查找支持。 这些工具已与Isabelle校样助手一体化。 Nitpick也可作为独立工具可用，接受TPTP THF语法。 该系统对于在问题编码中曝光错误和误解以及揭示THF定理普通的错误，该系统特别有价值。

5.应用程序

除了优雅，教堂的类型理论还具有许多实际优势。 例如，在农民（2023年）最近的教科书中强调了这一方面，这些教科书涉及本文中无法涵盖的各种相关和重要的进一步方面。 由于其良好的实用性表达，教会类型理论的应用范围非常广泛，下面只有几个例子

5.1自然语言的语义

教会的类型理论在自然语言正式语义的研究中起着重要作用。 在理查德蒙塔格圭完成了这一点。 将他的论文“作为一种正式的语言”，“普通语法”和“普通英语的正确治疗”，在蒙塔格1974年重印。蒙塔古对自然语言分析的关键组成部分是张力的定义海洋逻辑（Montague 1974：256），这是教会类型理论的增强。 Montague语法产生了巨大影响，并且已经在许多进一步的方向上发展，尤其是在TypeLical / CateLical语法中。 关于强度和高阶模态逻辑的进一步相关工作在Gallin 1975和Muskens 2006中介绍。

5.2数学与计算机科学

基于教堂的类型理论的证明助手，包括伊莎贝尔/霍尔，HOL，HOL光，HOL4和PVS，在计算机科学和数学的广泛应用中成功地利用。

计算机科学中的应用包括验证硬件，软件和安全协议。 一个突出的例子是L4.使用Isabelle / HOL正式证明SEL4操作系统内核的验证项目实现了一个抽象的数学模型，指定了内核所做的事情（Klein等，2018）。

在数学证明助理方面已经申请了图书馆数学理论的发展和挑战定理的验证。 早期示例是自TPS项目中八十年代以来开发的数学库。 在Andrews等人中给出了使用TPS自动证明的定理列表。 1996年。最近的一个非常突出的例子是Hales Flyspeck，其中霍尔灯被用来开发Kepler猜想的正式证据（Hales等，2017）。 在Benzmüller＆Scott 2019中介绍了强大地利用Sledgehammer和Nitpick在Isabelle / Hol中强烈利用自动化支持的示例。在这项工作中，探讨了各种类别理论的不同公理系统。

过去和正在进行的正式化项目的坚实概述，可以通过咨询伊莎贝尔档案的正式证明，“正式的TPTP问题图书馆”的正式证明杂志等适当的来源，如Isabelle的档案。 在Bentkamp等人中也可以找到相关的更多信息和讨论影响和进一步的工作。 2023B和Bayer等人。 2024。

基于拳击工具的证明辅助工具或其他形式的先驱集成在这些证明助手中进一步提高了自动化 - 与最大限度地减少未来应用中的互动工作。

5.3计算形而上学和人工智能

教堂的类型理论是一种古典逻辑，但哲学和人工智能的局部应用程序通常需要表现力的非典型逻辑。 为了支持具有教会类型理论的推理工具的此类应用，已经开发了浅层语义嵌入技术（另见第1.2.2节），以概括并扩展到众所周知的模态逻辑标准翻译的思想呈现给一阶逻辑。 该技术用于评估本体论论证的现代变体，包括一系列高级定理普罗维者，包括Leo-II，Satallax，Nitpick和Isabelle / Hol。 在实验过程中，Leo-II检测到哥德尔的论证的处所不一致，而普罗瓦斯成功地自动证明斯科特的修改并确认了所强制的场所的一致性。 有关此工作的更多详细信息，请参阅自动推理的相关SEP条目（参见逻辑和哲学的第4.6节）。 语义嵌入方法已经适用，进一步扩展了一系列其他非古典逻辑和相关应用。 在哲学中，这包括对雄心勃勃的道德和形而上学理论的编码和正式评估，并且在人工智能中，这包括语法的机械化和规范性推理来控制AI系统（Benzmüller等，2020）以及泥泞儿童难题的自动证明（参见动态认知逻辑的附录B），这是一个在认知推理中的着名拼图，分别是动态的认知推理。

5.4。 金属研究

教会的类型理论也非常适合支持融合性研究，包括编码其他逻辑形式主义和正式的声音和完整性研究（参见，例如，Schlichtkrull等。2020，Halkjær等2023，和在Benzmüller2019中给出的各种其他指针）。 特别是，教堂的类型理论可以本身可以自行研究，例如由Kumar等人所示。 （2016），Schlichtkrull（2023）和Díaz（2023）。