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 条
  • [21] Some Remarks on the Proof-Theory and the Semantics of Infinitary Modal Logic
    Minari, Pierluigi
    ADVANCES IN PROOF THEORY, 2016, 28 : 291 - 318
  • [22] A Machine-Checked Implementation of Buchberger's Algorithm
    Laurent Théry
    Journal of Automated Reasoning, 2001, 26 : 107 - 137
  • [23] Machine-Checked Proofs for Realizability Checking Algorithms
    Katis, Andreas
    Gacek, Andrew
    Whalen, Michael W.
    VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, 2016, 9593 : 110 - 123
  • [24] PROOF-THEORY AND COMPLEXITY
    CELLUCCI, C
    SYNTHESE, 1985, 62 (02) : 173 - 189
  • [25] Machine-checked model for Micro-Dalvik virtual machine
    He, Yan-Xiang
    Jiang, Nan
    Li, Qing-An
    Zhang, Jun
    Shen, Fan-Fan
    Ruan Jian Xue Bao/Journal of Software, 2015, 26 (02): : 364 - 379
  • [26] A machine-checked implementation of Buchberger's algorithm
    Théry, L
    JOURNAL OF AUTOMATED REASONING, 2001, 26 (02) : 107 - 137
  • [27] A Machine-Checked Formalization of Sigma-Protocols
    Barthe, Gilles
    Hedin, Daniel
    Zanella Beguelin, Santiago
    Gregoire, Benjamin
    Heraud, Sylvain
    2010 23RD IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2010, : 246 - 260
  • [28] A machine-checked formalization of the random oracle model
    Barthe, G
    Tarento, S
    TYPES FOR PROOFS AND PROGRAMS, 2006, 3839 : 33 - 49
  • [29] TOWARDS A PROOF THEORY OF GODEL MODAL LOGICS
    Metcalfe, George
    Olivetti, Nicola
    LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (02)
  • [30] Proof theory for quantified monotone modal logics
    Negri, Sara
    Orlandelli, Eugenio
    LOGIC JOURNAL OF THE IGPL, 2019, 27 (04) : 478 - 506
12345