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 条

[31] PROOF-THEORY AND SET-THEORY
TAKEUTI, G
SYNTHESE, 1985, 62 (02) : 255 - 263
[32] On the Proof-Theory of two Formalisations of Modal First-Order Logic
Schwartz, Yehuda
Tourlakis, George
STUDIA LOGICA, 2010, 96 (03) : 349 - 373
[33] Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory
Copello, Ernesto
Szasz, Nora
Tasistro, Alvaro
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2018, 338 : 79 - 95
[34] On the Proof-Theory of two Formalisations of Modal First-Order Logic
Yehuda Schwartz
George Tourlakis
Studia Logica, 2010, 96 : 349 - 373
[35] Machine-checked security proofs of cryptographic signature schemes
Tarento, S
COMPUTER SECURITY - ESORICS 2005, PROCEEDINGS, 2005, 3679 : 140 - 158
[36] Machine-Checked Proofs of Privacy for Electronic Voting Protocols
Cortier, Veronique
Dragan, Constantin Catalin
Dupressoir, Francois
Schmidt, Benedikt
Strub, Pierre-Yves
Warinschi, Bogdan
2017 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP), 2017, : 993 - 1008
[37] Machine-Checked Sequencer for Critical Embedded Code Generator
Izerrouken, Nassima
Pantel, Marc
Thirioux, Xavier
FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5885 : 521 - 540
[38] Practical Machine-Checked Formalization of Change Impact Analysis
Palmskog, Karl
Celik, Ahmet
Gligoric, Milos
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 : 137 - 157
[39] Automated Machine-Checked Hybrid System Safety Proofs
Geuvers, Herman
Koprowski, Adam
Synek, Dan
van der Weegen, Eelis
INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 259 - +
[40] Towards a machine-checked Java']Java specification book
Reus, B
Hein, T
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 480 - 497

← 1 2 3 4 5 →