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 条
  • [41] Refutation systems for propositional modal logics
    Miglioli, P
    Moscato, U
    Ornaghi, M
    THEOREM PROVING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 1995, 918 : 95 - 105
  • [42] Decidability by Resolution for Propositional Modal Logics
    Renate A. Schmidt
    Journal of Automated Reasoning, 1999, 22 : 379 - 396
  • [43] Decidability by resolution for propositional modal logics
    Schmidt, RA
    JOURNAL OF AUTOMATED REASONING, 1999, 22 (04) : 379 - 396
  • [44] Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+
    Barbosa, Manuel
    Dupressoir, Francois
    Gregoire, Benjamin
    Hulsing, Andreas
    Meijers, Matthias
    Strub, Pierre-Yves
    ADVANCES IN CRYPTOLOGY - CRYPTO 2023, PT V, 2023, 14085 : 421 - 454
  • [45] A machine-checked formalization of the generic model and the random oracle model
    Barthe, G
    Cederquist, J
    Tarento, S
    AUTOMATED REASONING, PROCEEDINGS, 2004, 3097 : 385 - 399
  • [46] WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms
    Veronese, Lorenzo
    Farinier, Benjamin
    Bernardo, Pedro
    Tempesta, Mauro
    Squarcina, Marco
    Maffei, Matteo
    2023 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, SP, 2023, : 2761 - 2779
  • [47] Efficient construction of machine-checked symbolic protocol security proofs
    Meier, Simon
    Cremers, Cas
    Basin, David
    JOURNAL OF COMPUTER SECURITY, 2013, 21 (01) : 41 - 87
  • [48] Java and the java memory model - A unified, machine-checked formalisation
    Karlsruher Institut für Technologie, Germany
    Lect. Notes Comput. Sci., (497-517):
  • [49] Proof-Theory and Semantics for a Theory of Definite Descriptions
    Kuerbis, Nils
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2021, 2021, 12842 : 95 - 111
  • [50] Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
    Cortier, Veronique
    Dragan, Constantin Catalin
    Dupressoir, Francois
    Warinschi, Bogdan
    IEEE 31ST COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2018), 2018, : 298 - 312
12345