Extending a High-Performance Prover to Higher-Order Logic

被引：2

作者：

Vukmirovic, Petar ^{[1
]}

Blanchette, Jasmin ^{[1
,2
]}

Schulz, Stephan ^{[3
]}

机构：

[1] Vrije Univ Amsterdam, Amsterdam, Netherlands

[2] Univ Lorraine, LORIA, INRIA, CNRS, Nancy, France

[3] DHBW Stuttgart, Stuttgart, Germany

来源：

TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2023 | 2023年 / 13994卷

基金：

欧洲研究理事会;

关键词：

FORMAL VERIFICATION;

D O I：

10.1007/978-3-031-30820-8_10

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Most users of proof assistants want more proof automation. Some proof assistants discharge goals by translating them to first-order logic and invoking an efficient prover on them, but much is lost in translation. Instead, we propose to extend first-order provers with native support for higher-order features. Building on our extension of E to lambda-free higher-order logic, we extend E to full higher-order logic. The result is the strongest prover on benchmarks exported from a proof assistant.

引用

页码：111 / 129

页数：19

共 50 条

[1] Extending a brainiac prover to lambda-free higher-order logic
Petar Vukmirović
Jasmin Blanchette
Simon Cruanes
Stephan Schulz
International Journal on Software Tools for Technology Transfer, 2022, 24 : 67 - 87
[2] Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
Vukmirovic, Petar
Blanchette, Jasmin Christian
Cruanes, Simon
Schulz, Stephan
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, 2019, 11427 : 192 - 210
[3] Extending a brainiac prover to lambda-free higher-order logic
Vukmirovic, Petar
Blanchette, Jasmin
Cruanes, Simon
Schulz, Stephan
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2022, 24 (01) : 67 - 87
[4] Implementing a program logic of objects in a higher-order logic theorem prover
Hofmann, M
Tang, F
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 268 - 282
[5] Extending SMT Solvers to Higher-Order Logic
Barbosa, Haniel
Reynolds, Andrew
El Ouraoui, Daniel
Tinelli, Cesare
Barrett, Clark
AUTOMATED DEDUCTION, CADE 27, 2019, 11716 : 35 - 54
[6] The Higher-Order Prover Leo-II
Christoph Benzmüller
Nik Sultana
Lawrence C. Paulson
Frank Theiß
Journal of Automated Reasoning, 2015, 55 : 389 - 404
[7] The Higher-Order Prover Leo-III
Steen, Alexander
Benzmueller, Christoph
ECAI 2020: 24TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2020, 325 : 2937 - 2938
[8] The Higher-Order Prover LEO-II
Benzmueller, Christoph
Sultana, Nik
Paulson, Lawrence C.
Theiss, Frank
JOURNAL OF AUTOMATED REASONING, 2015, 55 (04) : 389 - 404
[9] The Higher-Order Prover Leo-III
Steen, Alexander
Benzmueller, Christoph
AUTOMATED REASONING, IJCAR 2018, 2018, 10900 : 108 - 116
[10] LEO-II -: A cooperative automatic theorem prover for classical higher-order logic
Benzmueller, Christoph
Paulson, Lawrence C.
Theiss, Frank
Fietzke, Arnaud
AUTOMATED REASONING, PROCEEDINGS, 2008, 5195 : 162 - +

← 1 2 3 4 5 →