Axiomatizing proof tree concepts in Bounded Arithmetic

Author Satoru Kuroda



PDF
Thumbnail PDF

File

LIPIcs.CSL.2012.440.pdf
  • Filesize: 390 kB
  • 15 pages

Document Identifiers

Author Details

Satoru Kuroda

Cite AsGet BibTex

Satoru Kuroda. Axiomatizing proof tree concepts in Bounded Arithmetic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 440-454, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/LIPIcs.CSL.2012.440

Abstract

We construct theories of Cook-Nguyen style two-sort bounded arithmetic whose provably total functions are exactly those in LOGCFL and LOGDCFL. Axiomatizations of both theories are based on the proof tree size characterizations of these classes. We also show that our theory for LOGCFL proves a certain formulation of the pumping lemma for context-free languages.
Keywords
  • Bounded Arithmetic
  • LOGCFL
  • LOGDCFL
  • Proof tree

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads