A formal framework for specifying sequent calculus proof systems

被引：28
作者：
Miller, Dale [1 ,2 ]
Pimentel, Elaine [3 ,4 ]
机构：
[1] INRIA Saclay, Palaiseau, France
[2] Ecole Polytech, LIX, Palaiseau, France
[3] Univ Valle, Dept Matemat, Cali, Colombia
[4] Univ Fed Minas Gerais, Dept Matemat, Belo Horizonte, MG, Brazil
来源：
THEORETICAL COMPUTER SCIENCE | 2013年 / 474卷
关键词：
Logical frameworks; Linear logic; Sequent calculus; Proof systems; Cut elimination; LOGIC; SPECIFICATION;
D O I：
10.1016/j.tcs.2012.12.008
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Intuitionistic logic and intuitionistic type systems are commonly used as frameworks for the specification of natural deduction proof systems. In this paper we show how to use classical linear logic as a logical framework to specify sequent calculus proof systems and to establish some simple consequences of the specified sequent calculus proof systems. In particular, derivability of an inference rule from a set of inference rules can be decided by bounded (linear) logic programming search on the specified rules. We also present two simple and decidable conditions that guarantee that the cut rule and non-atomic initial rules can be eliminated. (C) 2012 Elsevier B.V. All rights reserved.
引用
收藏
页码：98 / 116
页数：19
相关论文
共 48 条
  • [1] Abrusci VM, 2000, ANN PURE APPL LOGIC, V101, P29, DOI 10.1016/S0168-0072(99)00014-7
  • [2] Andreoli J. M., 1992, Journal of Logic and Computation, V2, P297, DOI 10.1093/logcom/2.3.297
  • [3] Focussing and proof construction
    Andreoli, JM
    [J]. ANNALS OF PURE AND APPLIED LOGIC, 2001, 107 (1-3) : 131 - 163
  • [4] [Anonymous], 1940, Journal of Symbolic Logic
  • [5] Avron A., 2001, Automated Reasoning. First International Joint Conference, IJCAR 2001. Proceedings (Lecture Notes in Artificial Intelligence Vol.2083), P529
  • [6] A linear logical framework
    Cervesato, I
    Pfenning, F
    [J]. INFORMATION AND COMPUTATION, 2002, 179 (01) : 19 - 75
  • [7] Towards a semantic characterization of cut-elimination
    Ciabattoni A.
    Terui K.
    [J]. Studia Logica, 2006, 82 (1) : 95 - 119
  • [8] From axioms to analytic rules in nonclassical logics
    Ciabattoni, Agata
    Galatos, Nikolaos
    Terui, Kazushige
    [J]. TWENTY-THIRD ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2008, : 229 - +
  • [9] PROVING TERMINATION WITH MULTI-SET ORDERINGS
    DERSHOWITZ, N
    MANNA, Z
    [J]. COMMUNICATIONS OF THE ACM, 1979, 22 (08) : 465 - 476
  • [10] CONTRACTION-FREE SEQUENT CALCULI FOR INTUITIONISTIC LOGIC
    DYCKHOFF, R
    [J]. JOURNAL OF SYMBOLIC LOGIC, 1992, 57 (03) : 795 - 807
12345