Towards a semantic characterization of cut-elimination

被引：27
作者：
Ciabattoni A. [1 ]
Terui K. [2 ]
机构：
[1] Institute für Computersprachen, TU Wien, 1040 Wien
[2] National Institute of Informatics, Chiyoda-ku 101-8430 Tokyo
来源：
Studia Logica | 2006年 / 82卷 / 1期
基金：
奥地利科学基金会;
关键词：
Cut-elimination; Nonclassical logicss; Phase semantics; Sequent calculus; Substructural logics;
D O I：
10.1007/s11225-006-6607-2
中图分类号：
学科分类号：
摘要：
We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically. © Springer 2006.
引用
收藏
页码：95 / 119
页数：24
相关论文
共 22 条
  • [1] Abrusci V.M., Non-commutative intuitionistic linear propositional logic, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 36, pp. 297-318, (1990)
  • [2] Avron A., Lev I., Canonical propositional gentzen-Type systems, Proceedings of IJCAR'01, 2083, pp. 529-543, (2001)
  • [3] Belardinelli F.H.O.N.O., Jipsen P., Algebraic aspects of cut elimination, Studia Logica, 68, pp. 1-32, (2001)
  • [4] Belnap Jr. N.D., Display logic, Journal of Philosophical Logic, 11, 4, pp. 375-417, (1982)
  • [5] Buss S., An introduction to proof theory, Handbook of Proof Theory, pp. 1-78, (1998)
  • [6] Ciabattoni A., Automated generation of analytic calculi for logics with linearity, Proceedings of CSL'04, 3210, pp. 503-517, (2004)
  • [7] Gentzen G., Untersuchungen über das logische schliessen, Math. Zeitschrift, 39, 176-210, pp. 405-431, (1935)
  • [8] Girard J.-Y., Three valued logics and cut-elimination: The actual meaning of Takeuti's conjecture, Dissertationes Mathematicae, 136, pp. 1-49, (1976)
  • [9] Glrard J.-Y., Proof Theory and Logical Complexity, (1987)
  • [10] Girard J.-Y., Lafont Y., Taylor P., Proofs and Types, (1989)
123