LEO II: An Effective Higher-Order Theorem Prover

自动定理证明器（ATP）是一个可以自动证明数学命题的软件。现代atp非常强大，经常处理涉及数千个独立事实的问题。atp可以应用于实际任务，如查找计算机程序中的故障。一般来说，使用数学逻辑来分析计算机设计称为形式验证。大多数atp的一个限制与表达数学陈述的语言有关。大多数atp接受一阶逻辑，它可以表达关于单个项目的断言，因为所有整数要么是偶数，要么是奇数。然而，数学中的许多命题很难在一阶逻辑中表达，特别是当它们涉及集合或函数时。高阶逻辑类似于一阶逻辑，但它有内置的集合和函数的概念。它广泛应用于形式验证中，对于表示计算机硬件设计的断言特别方便。不幸的是，高阶逻辑只有一个ATP；它建于20世纪80年代，以现代标准衡量，它的性能很差。一种被称为LEO的实验性高阶ATP最近显示出了希望；在最近的工作中，它已经与传统的ATP结合在一起，这样它就可以从后者的高性能中受益。该提案是采用最近在LEO中原型化的想法，并将其用作强大的新高阶ATP的基础。它旨在用于正式验证的应用，但该项目也将阐明高阶逻辑机械化中的基本问题。

An Automatic Theorem Prover (ATP) is a piece of software that can prove mathematical statements automatically. Modern ATPs are impressively powerful, often coping with problems that involve thousands of separate facts. ATPs can be applied to practical tasks such as finding faults in computer programs. In general, the use of mathematical logic to analyse computer designs is called formal verification.One limitation of most ATPs concerns the language in which the mathematical statements are expressed. Most ATPs accept first-order logic, which can express assertions about individual items, as in all integers are either even or odd . However, many statements in mathematics are difficult to express in first-order logic, especially if they refer to sets or functions.Higher-order logic resembles first-order logic, but it has built-in notions of sets and functions. It is widely used in formal verification, being especially convenient for expressing assertions about computer hardware designs. Unfortunately, there is only one ATP for higher-order logic; it dates from the 1980s and its performance is poor by modern standards. An experimental higher-order ATP, called LEO, has recently shown promise; in recent work, it has been combined with a conventional ATP so that it can benefit from the latter's high performance.The proposal is to take the ideas recently prototyped in LEO and use them as the basis for a robust new higher-order ATP. It is intended for applications in formal verification, but the project will also shed light on fundamental issues in the mechanization of higher-order logic.