REPRESENTING HIGHER-ORDER LOGIC PROOFS IN HOL

被引：2
|
作者：
VONWRIGHT, J
机构：
[1] Abo Akademi Univ, Turku
来源：
COMPUTER JOURNAL | 1995年 / 38卷 / 02期
关键词：
D O I：
10.1093/comjnl/38.2.171
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We describe an embedding of higher order logic in the HOL theorem proving system. Types, terms, sequents and inferences are represented as new types in the logic of the HOL system, and notions of proof and provability are defined. Using this formalisation, it is possible to reason about the correctness of derived rules of inference and about the relations between different notions of proofs. The formalisation is also intended to make it possible to reason about programs that handle proofs as their data (e.g., proof checkers).
引用
收藏
页码：171 / 179
页数：9
相关论文
共 50 条
  • [1] EXPANSION TREE PROOFS IN HIGHER-ORDER LOGIC
    MILLER, DA
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1984, 49 (04) : 1443 - 1444
  • [2] Program logic for higher-order probabilistic programs in Isabelle/HOL
    Hirata, Michikazu
    Minamide, Yasuhiko
    Sato, Tetsuya
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2023, 230
  • [3] Interactive Proofs in Higher-Order Concurrent Separation Logic
    Krebbers, Robbert
    Timany, Amin
    Birkedal, Lars
    [J]. ACM SIGPLAN NOTICES, 2017, 52 (01) : 205 - 217
  • [4] PNL to HOL: From the logic of nominal sets to the logic of higher-order functions
    Dowek, Gilles
    Gabbay, Murdoch J.
    [J]. THEORETICAL COMPUTER SCIENCE, 2012, 451 : 38 - 69
  • [5] CryptHOL: Game-Based Proofs in Higher-Order Logic
    David A. Basin
    Andreas Lochbihler
    S. Reza Sefidgar
    [J]. Journal of Cryptology, 2020, 33 : 494 - 566
  • [6] CryptHOL: Game-Based Proofs in Higher-Order Logic
    Basin, David A.
    Lochbihler, Andreas
    Sefidgar, S. Reza
    [J]. JOURNAL OF CRYPTOLOGY, 2020, 33 (02) : 494 - 566
  • [7] EXECUTING HOL SPECIFICATIONS - TOWARDS AN EVALUATION SEMANTICS FOR CLASSICAL HIGHER-ORDER LOGIC
    RAJAN, PS
    [J]. IFIP TRANSACTIONS A-COMPUTER SCIENCE AND TECHNOLOGY, 1993, 20 : 527 - 536
  • [8] ON THE ADEQUACY OF REPRESENTING HIGHER-ORDER INTUITIONISTIC LOGIC AS A PURE TYPE SYSTEM
    TONINO, H
    FUJITA, K
    [J]. ANNALS OF PURE AND APPLIED LOGIC, 1992, 57 (03) : 251 - 276
  • [9] Higher-order logic programming: An expressive language for representing qualitative preferences
    Charalambidis, Angelos
    Rondogiannis, Panos
    Troumpoukis, Antonis
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2018, 155 : 173 - 197
  • [10] Higher-Order Abstract Syntax in Isabelle/HOL
    Howe, Douglas J.
    [J]. INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 481 - 484
12345