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 条
  • [31] EXTENDING THE IMAGE METHOD TO HIGHER-ORDER REFLECTIONS
    KRISTIANSEN, UR
    KROKSTAD, A
    FOLLESTAD, T
    APPLIED ACOUSTICS, 1993, 38 (2-4) : 195 - 206
  • [32] A NOTE ON THE LOGIC OF (HIGHER-ORDER) VAGUENESS
    HECK, RG
    ANALYSIS, 1993, 53 (04) : 201 - 208
  • [33] On Models of Higher-Order Separation Logic
    Bizjak, Ales
    Birkedal, Lars
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2018, 336 : 57 - 78
  • [34] Superposition for Full Higher-order Logic
    Bentkamp, Alexander
    Blanchette, Jasmin
    Tourret, Sophie
    Vukmirovic, Petar
    AUTOMATED DEDUCTION, CADE 28, 2021, 12699 : 396 - 412
  • [35] Topological completeness for higher-order logic
    Awodey, S
    Butz, C
    JOURNAL OF SYMBOLIC LOGIC, 2000, 65 (03) : 1168 - 1182
  • [36] Modal Pluralism and Higher-Order Logic
    Clarke-Doane, Justin
    McCarthy, William
    PHILOSOPHICAL PERSPECTIVES, 2022, 36 (01) : 31 - 58
  • [37] SOME REMARKS ON HIGHER-ORDER LOGIC
    KOGALOVSKII, SR
    DOKLADY AKADEMII NAUK SSSR, 1968, 178 (05): : 1007 - +
  • [38] Learning higher-order logic programs
    Andrew Cropper
    Rolf Morel
    Stephen Muggleton
    Machine Learning, 2020, 109 : 1289 - 1322
  • [39] RESULTS IN HIGHER-ORDER MODAL LOGIC
    GALLIN, D
    JOURNAL OF SYMBOLIC LOGIC, 1974, 39 (01) : 197 - 198
  • [40] Higher-order modal logic - A sketch
    Fitting, H
    AUTOMATED DEDUCTION IN CLASSICAL AND NON-CLASSICAL LOGICS, 2000, 1761 : 23 - 38
12345