A verified proof checker for higher-order logic

被引：4
|
作者：
Abrahamsson, Oskar [1 ]
机构：
[1] Chalmers Univ Technol, Dept Comp Sci & Engn, SE-41296 Gothenburg, Sweden
来源：
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING | 2020年 / 112卷
关键词：
Proof checker; Higher-order logic; Mechanized proof; Soundness; THEOREM PROVER; SOUND;
D O I：
10.1016/j.jlamp.2020.100530
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We present a computer program for checking proofs in higher-order logic (HOL) that is verified to accept only valid proofs. The proof checker is defined as functions in HOL and synthesized to CakeML code, and uses the Candle theorem prover kernel to check logical inferences. The checker reads proofs in the OpenTheory article format, which means proofs produced by various HOL proof assistants are supported. The proof checker is implemented and verified using the HOL4 theorem prover, and comes with a proof of soundness. (C) 2020 Elsevier Inc. All rights reserved.
引用
收藏
页数：19
相关论文
共 50 条
  • [1] Effect Polymorphism in Higher-Order Logic (Proof Pearl)
    Lochbihler, Andreas
    [J]. INTERACTIVE THEOREM PROVING (ITP 2017), 2017, 10499 : 389 - 409
  • [2] Effect Polymorphism in Higher-Order Logic (Proof Pearl)
    Andreas Lochbihler
    [J]. Journal of Automated Reasoning, 2019, 63 : 439 - 462
  • [3] Effect Polymorphism in Higher-Order Logic (Proof Pearl)
    Lochbihler, Andreas
    [J]. JOURNAL OF AUTOMATED REASONING, 2019, 63 (02) : 439 - 462
  • [4] Proof-theoretic and higher-order extensions of logic programming
    Momigliano A.
    Ornaghi M.
    [J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2010, 6125 : 254 - 270
  • [5] Verified Proofs of Higher-Order Masking
    Barthe, Gilles
    Belaid, Sonia
    Dupressoir, Francois
    Fouque, Pierre-Alain
    Gregoire, Benjamin
    Strub, Pierre-Yves
    [J]. ADVANCES IN CRYPTOLOGY - EUROCRYPT 2015, PT I, 2015, 9056 : 457 - 485
  • [6] Self-Formalisation of Higher-Order Logic Semantics, Soundness, and a Verified Implementation
    Kumar, Ramana
    Arthan, Rob
    Myreen, Magnus O.
    Owens, Scott
    [J]. JOURNAL OF AUTOMATED REASONING, 2016, 56 (03) : 221 - 259
  • [7] ON HIGHER-ORDER LOGIC
    KOGALOVS.SR
    [J]. DOKLADY AKADEMII NAUK SSSR, 1966, 171 (06): : 1272 - &
  • [8] MECHANIZING A PROOF BY INDUCTION OF PROCESS ALGEBRA SPECIFICATIONS IN HIGHER-ORDER LOGIC
    NESI, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 575 : 288 - 298
  • [9] A proof-theoretic foundation for tabled higher-order logic programming
    Pientka, B
    [J]. LOGICS PROGRAMMING, PROCEEDINGS, 2002, 2401 : 271 - 286
  • [10] Proof-Producing Synthesis of ML from Higher-Order Logic
    Myreen, Magnus O.
    Owens, Scott
    [J]. ACM SIGPLAN NOTICES, 2012, 47 (09) : 115 - 126
12345