Machine-Checked Proof-Theory for Propositional Modal Logics

被引：0
|
作者：
Dawson, Jeremy E. [1 ]
Gore, Rajeev [1 ]
Wu, Jesse [1 ]
机构：
[1] Australian Natl Univ, Sch Comp Sci, Log & Computat Grp, Canberra, ACT 2601, Australia
来源：
ADVANCES IN PROOF THEORY | 2016年 / 28卷
关键词：
D O I：
10.1007/978-3-319-29198-7_5
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We describe how we machine-checked the admissibility of the standard structural rules of weakening, contraction and cut for multiset-based sequent calculi for the unimodal logics S4, S4.3 and K4De, as well as for the bimodal logic S4C recently investigated by Mints. Our proofs for both S4 and S4.3 appear to be new while our proof for S4C is different from that originally presented by Mints, and appears to avoid the complications he encountered. The paper is intended to be an overview of how to machine-check proof theory for readers with a good understanding of proof theory.
引用
收藏
页码：173 / 243
页数：71
相关论文
共 50 条
  • [1] A machine-checked correctness proof for Pastry
    Azmy, Noran
    Merz, Stephan
    Weidenbach, Christoph
    SCIENCE OF COMPUTER PROGRAMMING, 2018, 158 : 64 - 80
  • [2] A Machine-Checked Proof of the Odd Order Theorem
    Gonthier, Georges
    Asperti, Andrea
    Avigad, Jeremy
    Bertot, Yves
    Cohen, Cyril
    Garillot, Francois
    Le Roux, Stephane
    Mahboubi, Assia
    O'Connor, Russell
    Biha, Sidi Ould
    Pasca, Ioana
    Rideau, Laurence
    Solovyev, Alexey
    Tassi, Enrico
    Thery, Laurent
    INTERACTIVE THEOREM PROVING, ITP 2013, 2013, 7998 : 163 - 179
  • [3] TRACKING DESIGN CHANGES WITH FORMAL MACHINE-CHECKED PROOF
    CURZON, P
    COMPUTER JOURNAL, 1995, 38 (02): : 91 - 100
  • [4] A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
    Kellison, Ariel
    PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22), 2022, : 265 - 273
  • [5] A machine-checked theory of floating point arithmetic
    Harrison, J
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 1999, 1690 : 113 - 130
  • [6] Classical and Fuzzy Two-Layered Modal Logics for Uncertainty: Translations and Proof-Theory
    Baldi, Paolo
    Cintula, Petr
    Noguera, Cartes
    INTERNATIONAL JOURNAL OF COMPUTATIONAL INTELLIGENCE SYSTEMS, 2020, 13 (01) : 988 - 1001
  • [7] Classical and Fuzzy Two-Layered Modal Logics for Uncertainty: Translations and Proof-Theory
    Paolo Baldi
    Petr Cintula
    Carles Noguera
    International Journal of Computational Intelligence Systems, 2020, 13 : 988 - 1001
  • [8] Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi
    Dawson, Jeremy E.
    Brotherston, James
    Gore, Rajeev
    AUTOMATED REASONING (IJCAR 2016), 2016, 9706 : 452 - 468
  • [9] A machine-checked soundness proof for an efficient verification condition generator
    Vogels, Frédéric
    Jacobs, Bart
    Piessens, Frank
    Proceedings of the ACM Symposium on Applied Computing, 2010, : 2517 - 2522
  • [10] A Machine-Checked Proof of Security for AWS Key Management Service
    Almeida, Jose Bacelar
    Barbosa, Manuel
    Barthe, Gilles
    Campagna, Matthew
    Cohen, Ernie
    Gregoire, Benjamin
    Pereira, Vitor
    Portela, Bernardo
    Strub, Pierre-Yves
    Tasiran, Serdar
    PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19), 2019, : 63 - 78
12345