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 条

[21] Superposition for Higher-Order Logic
Alexander Bentkamp
Jasmin Blanchette
Sophie Tourret
Petar Vukmirović
Journal of Automated Reasoning, 2023, 67
[22] Superposition for Higher-Order Logic
Bentkamp, Alexander
Blanchette, Jasmin
Tourret, Sophie
Vukmirovic, Petar
JOURNAL OF AUTOMATED REASONING, 2023, 67 (01)
[23] Higher-Order Coalition Logic
Boella, Guido
Gabbay, Dov M.
Genovese, Valerio
van der Torre, Leendert
ECAI 2010 - 19TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2010, 215 : 555 - 560
[24] A logic of higher-order preferences
Jiang, Junli
Naumov, Pavel
SYNTHESE, 2024, 203 (06)
[25] The Higher-Order Prover Leo-III (Extended Abstract)
Steen, Alexander
Benzmueller, Christoph
ADVANCES IN ARTIFICIAL INTELLIGENCE, KI 2019, 2019, 11793 : 333 - 337
[26] Higher-order compact scheme for high-performance computing of stratified rotating flows
Abide, Stephane
Viazzo, Stephane
Raspo, Isabelle
Randriamampianina, Anthony
COMPUTERS & FLUIDS, 2018, 174 : 300 - 310
[27] On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
Kobayashi, Naoki
Lozes, Etienne
Bruse, Florian
ACM SIGPLAN NOTICES, 2017, 52 (01) : 246 - 259
[28] Extensional Higher-Order Logic Programming
Charalambidis, Angelos
Handjopoulos, Konstantinos
Rondogiannis, Panos
Wadge, William W.
LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2010, 2010, 6341 : 91 - 103
[29] HAUPTSATZ FOR HIGHER-ORDER MODAL LOGIC
NISHIMURA, H
JOURNAL OF SYMBOLIC LOGIC, 1983, 48 (03) : 744 - 751
[30] Partiality and Recursion in Higher-Order Logic
Czajka, Lukasz
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2013), 2013, 7794 : 177 - 192

← 1 2 3 4 5 →