TY - JOUR
T1 - Applicative theories for logarithmic complexity classes
JF - Theoretical Computer Science
Y1 - 2015
A1 - Sebastian Eberhard
AB - We present applicative theories of words corresponding to weak, and especially logarithmic, complexity classes. The theories for the logarithmic hierarchy and alternating logarithmic time formalise function algebras with concatenation recursion as main principle. We present two theories for logarithmic space where the first formalises a new two-sorted algebra which is very similar to Cook and Bellantoni's famous two-sorted algebra B for polynomial time [4]. The second theory describes logarithmic space by formalising concatenation- and sharply bounded recursion. All theories contain the predicates WW representing words, and VV representing temporary inaccessible words. They are inspired by Cantini's theories [6] formalising B.
PB - Elsevier
VL - 585
UR - http://www.iam.unibe.ch/ltgpub/2015/ebat15.pdf
ER -
TY - CHAP
T1 - Unfolding Feasible Arithmetic and Weak Truth
T2 - Unifying the Philosophy of Truth
Y1 - 2015
A1 - Sebastian Eberhard
A1 - Thomas Strahm
ED - Theodora Achourioti
ED - Henri Galinon
ED - José Martínez Fernández
ED - Kentaro Fujimoto
AB - In this paper we continue Feferman?s unfolding program initiated in (Feferman, vol. 6 of Lecture Notes in Logic, 1996) which uses the concept of the unfolding U(S) of a schematic system S in order to describe those operations, predicates and principles concerning them, which are implicit in the acceptance of S. The program has been carried through for a schematic system of non-finitist arithmetic NFA in Feferman and Strahm (Ann Pure Appl Log, 104(1?3):75?96, 2000) and for a system FA (with and without Bar rule) in Feferman and Strahm (Rev Symb Log, 3(4):665?689, 2010). The present contribution elucidates the concept of unfolding for a basic schematic system FEA of feasible arithmetic. Apart from the operational unfolding U0(FEA) of FEA, we study two full unfolding notions, namely the predicate unfolding U(FEA) and a more general truth unfolding UT(FEA) of FEA, the latter making use of a truth predicate added to the language of the operational unfolding. The main results obtained are that the provably convergent functions on binary words for all three unfolding systems are precisely those being computable in polynomial time. The upper bound computations make essential use of a specific theory of truth TPT over combinatory logic, which has recently been introduced in Eberhard and Strahm (Bull Symb Log, 18(3):474?475, 2012) and Eberhard (A feasible theory of truth over combinatory logic, 2014) and whose involved proof-theoretic analysis is due to Eberhard (A feasible theory of truth over combinatory logic, 2014). The results of this paper were first announced in (Eberhard and Strahm, Bull Symb Log 18(3):474?475, 2012).
JF - Unifying the Philosophy of Truth
T3 - Logic, Epistemology, and the Unity of Science
PB - Springer Netherlands
CY - Dordrecht
VL - 36
UR - http://www.iam.unibe.ch/ltgpub/2015/esu15.pdf
ER -
TY - JOUR
T1 - A feasible theory of truth over combinatory algebra
JF - Annals of Pure and Applied Logic
Y1 - 2014
A1 - Sebastian Eberhard
KW - Truth theories
VL - 165
UR - http://www.iam.unibe.ch/ltgpub/2012/ebe12a.pdf
ER -
TY - Generic
T1 - Weak applicative theories, truth, and computational complexity
Y1 - 2013
A1 - Sebastian Eberhard
PB - Universität Bern
CY - Institut für Informatik und angewandte Mathematik
UR - http://www.iam.unibe.ch/ltgpub/2013/ebe13.pdf
ER -
TY - CONF
T1 - Weak theories of truth and explicit mathematics
T2 - Logic, Construction, Computation
Y1 - 2012
A1 - Sebastian Eberhard
A1 - Thomas Strahm
ED - Ulrich Berger
ED - Hannes Diener
ED - Peter Schuster
ED - Monika Seisenberger
JF - Logic, Construction, Computation
PB - Ontos Verlag
UR - http://www.iam.unibe.ch/ltgpub/2012/es12a.pdf
ER -
TY - Generic
T1 - Aspekte beweisbar totaler Funktionen in applikativen Theorien
Y1 - 2009
A1 - Sebastian Eberhard
PB - Universität Bern
CY - Institut für Informatik und angewandte Mathematik
UR - http://www.iam.unibe.ch/ltgpub/2009/ebe09.pdf
ER -