权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

LEO II: An Effective Higher-Order Theorem Prover

LEO II：有效的高阶定理证明者

基本信息

批准号：
EP/D070511/1
负责人：
Lawrence Paulson
金额：
$ 11.79万
依托单位：
University of Cambridge
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2006
资助国家：
英国
起止时间：
2006 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FD070511%2F1
关键词：
LEO II Effective Higher Order

项目摘要

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.

自动定理证明器（ATP）是一个可以自动证明数学陈述的软件。现代ATP的功能强大得令人印象深刻，通常可以处理涉及数千个独立事实的问题。ATP可以应用于实际任务，如查找计算机程序中的错误。一般来说，使用数学逻辑来分析计算机设计被称为形式验证。大多数ATP的一个局限性涉及表达数学语句的语言。大多数ATP接受一阶逻辑，它可以表达关于单个项的断言，因为所有整数都是偶数或奇数。然而，数学中的许多陈述很难用一阶逻辑表达，特别是当它们涉及集合或函数时。高阶逻辑类似于一阶逻辑，但它有内置的集合和函数的概念。它被广泛应用于形式化验证，特别是方便表示有关计算机硬件设计的断言。不幸的是，高阶逻辑只有一个ATP;它可以追溯到20世纪80年代，按照现代标准，它的性能很差。一个实验性的高阶ATP，称为LEO，最近已经显示出了希望;在最近的工作中，它已经与传统的ATP相结合，以便它可以受益于后者的高性能。该建议是采取的想法最近原型在LEO和使用它们作为一个强大的新的高阶ATP的基础。它的目的是在形式验证的应用程序，但该项目也将揭示高阶逻辑的机械化的基本问题。