Extension without cut

Article English OPEN
Straßburger , Lutz;
(2012)
  • Publisher: Elsevier BV
  • Journal: Annals of Pure and Applied Logic,volume 163,issue 12,pages1,995-2,007 (issn: 0168-0072)
  • Publisher copyright policies & self-archiving
  • Related identifiers: doi: 10.1016/j.apal.2012.07.004
  • Subject: [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] | Logic
    arxiv: Computer Science::Logic in Computer Science | Mathematics::Logic

International audience; In proof theory one distinguishes sequent proofs with cut and cut-free sequent proofs, while for proof complexity one distinguishes Frege-systems and extended Frege-systems. In this paper we show how deep inference can provide a uniform treatment... View more
  • References (26)
    26 references, page 1 of 3

    [1] S. A. Cook, R. A. Reckhow, The relative efficiency of propositional proof systems, The Journal of Symbolic Logic 44 (1) (1979) 36-50.

    [2] A. S. Troelstra, H. Schwichtenberg, Basic Proof Theory, 2nd Edition, Cambridge University Press, 2000.

    [3] G. Gentzen, Untersuchungen u¨ber das logische Schließen. I., Mathematische Zeitschrift 39 (1934) 176-210.

    [4] M. Baaz, S. Hetzl, A. Leitsch, C. Richter, H. Spohr, Proof transformation by CERES, in: MKM'06, Vol. 4108 of LNCS, Springer, 2006, pp. 82-93.

    [5] R. Statman, Bounds for proof-search and speed-up in predicate calculus, Annals of Mathematical Logic 15 (1978) 225-287.

    [6] A. Haken, The intractability of resolution, TCS 39 (1985) 297-308.

    [7] M. Baaz, A. Leitsch, Towards a clausal analysis of cut-elimination, J. Symb. Comput. 41 (3-4) (2006) 381-410.

    [8] A. Ciabattoni, A. Leitsch, Towards an algorithmic construction of cut-elimination procedures, Math. Structures in Comp. Science 18 (1) (2008) 81-105.

    [9] A. Guglielmi, A system of interaction and structure, ACM Transactions on Computational Logic 8 (1) (2007) 1-64.

    [10] A. Guglielmi, L. Straßburger, Non-commutativity and MELL in the calculus of structures, in: L. Fribourg (Ed.), Computer Science Logic, CSL 2001, Vol. 2142 of LNCS, Springer-Verlag, 2001, pp. 54-68.

  • Metrics
Share - Bookmark