A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic

被引：0

作者：

Brian Hill

Francesca Poggiolesi

机构：

[1] Vrije Universiteit Brussel,Center of Logic and Philosophy of Science (CLFW)

[2] HEC Paris and IHPST (CNRS / Paris 1 / ENS),undefined

来源：

Studia Logica | 2010年 / 94卷

关键词：

Contraction-free; Cut-free; Propositional Dynamic Logic; Tree-hypersequent; Proof theory;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

In this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way.

引用

页码：47 / 72

页数：25

共 50 条

[41] A cut-free sequent system for two-dimensional modal logic, and why it matters
Restall, Greg
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2012, 163 (11) : 1611 - 1623
[42] Cut-free Gentzen calculus for multimodal CK
Mendler, Michael
Scheele, Stephan
[J]. INFORMATION AND COMPUTATION, 2011, 209 (12) : 1465 - 1490
[43] Proof Complexity of the Cut-free Calculus of Structures
Jerabek, Emil
[J]. JOURNAL OF LOGIC AND COMPUTATION, 2009, 19 (02) : 323 - 339
[44] A CUT-FREE CALCULUS FOR DUMMETTS LC QUANTIFIED
CORSI, G
[J]. ZEITSCHRIFT FUR MATHEMATISCHE LOGIK UND GRUNDLAGEN DER MATHEMATIK, 1989, 35 (04): : 289 - 301
[45] Modular Construction of Cut-Free Sequent Calculi for Paraconsistent Logics
Avron, Arnon
Konikowska, Beata
Zamansky, Anna
[J]. 2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 85 - 94
[46] A cut-free sequent system for Grzegorczyk logic, with an application to the Godel-McKinsey-Tarski embedding
Dyckhoff, Roy
Negri, Sara
[J]. JOURNAL OF LOGIC AND COMPUTATION, 2016, 26 (01) : 169 - 187
[47] A coding method for a sequent calculus of propositional logic
Alonderis, R.
[J]. LITHUANIAN MATHEMATICAL JOURNAL, 2008, 48 (02) : 123 - 136
[48] A coding method for a sequent calculus of propositional logic
R. Alonderis
[J]. Lithuanian Mathematical Journal, 2008, 48 : 123 - 136
[49] Cut-free formulations for a quantified logic of here and there
Mints, Grigori
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2010, 162 (03) : 237 - 242
[50] Is cut-free logic fit for unrestricted abstraction?
Petersen, Uwe
[J]. ANNALS OF PURE AND APPLIED LOGIC, 2022, 173 (06)

← 1 2 3 4 5 →