License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CSL.2012.440
URN: urn:nbn:de:0030-drops-36893
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3689/
Go to the corresponding LIPIcs Volume Portal

Kuroda, Satoru

Axiomatizing proof tree concepts in Bounded Arithmetic

pdf-format:
35.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{kuroda:LIPIcs:2012:3689,
  author =	{Satoru Kuroda},
  title =	{{Axiomatizing proof tree concepts in Bounded Arithmetic}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{440--454},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{Patrick C{\'e}gielski and Arnaud Durand},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3689},
  URN =		{urn:nbn:de:0030-drops-36893},
  doi =		{10.4230/LIPIcs.CSL.2012.440},
  annote =	{Keywords: Bounded Arithmetic, LOGCFL, LOGDCFL, Proof tree}
}

Keywords: Bounded Arithmetic, LOGCFL, LOGDCFL, Proof tree
Collection: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL
Issue Date: 2012
Date of publication: 03.09.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI