LIPIcs.CSL.2012.440.pdf
- Filesize: 390 kB
- 15 pages
Document
Axiomatizing proof tree concepts in Bounded Arithmetic
Author
-
Part of:
Volume:
Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (CSL 2012)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2012-09-03
Cite As Get 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.
Subject Classification
Keywords
- Bounded Arithmetic
- LOGCFL
- LOGDCFL
- Proof tree
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads