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 条

[41] HIGHER-ORDER ILLATIVE COMBINATORY LOGIC
Czajka, Lukasz
JOURNAL OF SYMBOLIC LOGIC, 2013, 78 (03) : 837 - 872
[42] ON NONSTANDARD MODELS IN HIGHER-ORDER LOGIC
HORT, C
OSSWALD, H
JOURNAL OF SYMBOLIC LOGIC, 1984, 49 (01) : 204 - 219
[43] Extensional Higher-Order Logic Programming
Charalambidis, Angelos
Handjopoulos, Konstantinos
Rondogiannis, Panagiotis
Wadge, William W.
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2013, 14 (03)
[44] Learning higher-order logic programs
Cropper, Andrew
Morel, Rolf
Muggleton, Stephen
MACHINE LEARNING, 2020, 109 (07) : 1289 - 1322
[45] HIGHER-ORDER LOGIC LEARNING AND λPROGOL
Pahlavi, Niels
TECHNICAL COMMUNICATIONS OF THE 26TH INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING (ICLP'10), 2010, 7 : 281 - 285
[46] REMARKS ON HIGHER-ORDER MODAL LOGIC
DACOSTA, NCA
DEALCANTARA, LP
ACTA CIENTIFICA VENEZOLANA, 1987, 38 (02): : 282 - 284
[47] Refinement of higher-order logic programs
Colvin, R
Hayes, I
Hemer, D
Strooper, P
LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2003, 2664 : 126 - 143
[48] Higher-Order Logic and Disquotational Truth
Picollo, Lavinia
Schindler, Thomas
JOURNAL OF PHILOSOPHICAL LOGIC, 2022, 51 (04) : 879 - 918
[49] Tabling for higher-order logic programming
Pientka, B
AUTOMATED DEDUCTION - CADE-20, PROCEEDINGS, 2005, 3632 : 54 - 68
[50] Functional procedures in higher-order logic
Laibinis, L
von Wright, J
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 372 - 387

← 1 2 3 4 5 →