@article {1780,
title = {A flexible type system for the small Veblen ordinal},
year = {Submitted},
url = {http://www.iam.unibe.ch/ltgpub/2016/rast16.pdf},
author = {Ranzi, Florian and Thomas Strahm}
}
@article {1902,
title = {From Mathesis Universalis to fixed points and related set-theoretic concepts},
year = {Submitted},
url = {http://www.iam.unibe.ch/ltgpub/2018/jast18.pdf},
author = {Gerhard J{\"a}ger and Silvia Steila}
}
@inbook {1898,
title = {A combinatorial bound for a restricted form of the Termination Theorem},
booktitle = {A unifying concept of proof theory, automata theory, formal languages and descriptive set theory},
year = {In Press},
publisher = {Springer},
organization = {Springer},
author = {Silvia Steila},
editor = {Peter Schuster and Monika Seisenberger and Andreas Weiermann}
}
@article {1921,
title = {Some algebraic equivalent forms of R ⊆ L},
journal = {Fundamenta Mathematicae},
year = {In Press},
url = {http://www.iam.unibe.ch/ltgpub/2018/ste18.pdf},
author = {Silvia Steila}
}
@conference {1916,
title = {A Decidable Multi-agent Logic with Iterations of Upper and Lower Probability Operators},
booktitle = {Foundations of Information and Knowledge Systems - 10th International Symposium, FoIKS 2018, Budapest, Hungary, May 14-18, 2018, Proceedings},
year = {2018},
pages = {170{\textendash}185},
url = {http://www.iam.unibe.ch/ltgpub/2018/dos18.pdf},
author = {Dragan Doder and Nenad Savi{\'c} and Zoran Ognjanovi{\'c}}
}
@article {1896,
title = {A Direct Proof of Schwichtenberg{\textquoteright}s Bar Recursion Closure Theorem},
journal = {The Journal of Symbolic Logic},
year = {2018},
pages = {1-14},
doi = {10.1017/jsl.2017.33},
url = {http://www.iam.unibe.ch/ltgpub/2017/os17.pdf},
author = {Paulo Oliva and Silvia Steila}
}
@conference {1897,
title = {A Logic of Blockchain Updates},
booktitle = {Logical Foundations of Computer Science},
year = {2018},
pages = {107-119},
publisher = {Springer International Publishing},
organization = {Springer International Publishing},
address = {Cham},
isbn = {978-3-319-72056-2},
url = {http://www.iam.unibe.ch/ltgpub/2018/bfs18.pdf},
author = {Kai Br{\"u}nnler and Dandolo Flumini and Thomas Studer},
editor = {Sergei Artemov and A. Nerode}
}
@article {1833,
title = {About some fixed point axioms and related principles in Kripke-Platek environments},
journal = {The Journal of Symbolic Logic},
volume = {83},
year = {2018},
pages = {642-668},
abstract = {Starting point of this article are fixed point axioms for set-bounded
monotone Σ_1 definable operators in the context of Kripke-Platek set
theory KP. We analyze their relationship to other principles such as
maximal iterations, bounded proper injections, and Σ_1 subset-bounded
sparation. One of our main results states that in KP + (V =L) all these
principles are equivalent to Σ_1 separation.},
url = {http://www.iam.unibe.ch/ltgpub/2017/jast17.pdf},
author = {Gerhard J{\"a}ger and Silvia Steila}
}
@conference {1917,
title = {Probabilistic Reasoning About Simply Typed Lambda Terms},
booktitle = {Logical Foundations of Computer Science - International Symposium, {LFCS} 2018, Deerfield Beach, FL, USA, January 8-11, 2018, Proceedings},
year = {2018},
pages = {170{\textendash}189},
url = {http://www.iam.unibe.ch/ltgpub/2018/gikos18.pdf},
author = {Silvia Ghilezan and Jelena Ivetic and Simona Kasterovic and Zoran Ognjanovi{\'c} and Nenad Savi{\'c}}
}
@article {1930,
title = {Some Models and Semi-decidability Notions of Applicative Theories},
year = {2018},
url = {http://www.iam.unibe.ch/ltgpub/2019/ros18.pdf},
author = {Timtej Rosebrock}
}
@inbook {1850,
title = {The Operational Penumbra: Some Ontological Aspects},
booktitle = {Feferman on Foundations - Logic, Mathematics, Philosophy},
volume = {13},
year = {2018},
publisher = {Springer International Publishing},
organization = {Springer International Publishing},
url = {http://www.iam.unibe.ch/ltgpub/2018/jae18.pdf},
author = {Gerhard J{\"a}ger}
}
@inbook {marti-studerCommon,
title = {The Proof Theory of Common Knowledge},
booktitle = {Jaakko Hintikka on knowledge and game theoretical semantics},
series = {Outstanding Contributions to Logic},
year = {2018},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2017/mast17.pdf},
author = {Michel Marti and Thomas Studer},
editor = {H. van Ditmarsch and G. Sandu}
}
@article {1894,
title = {The strength of SCT soundness},
journal = {Journal of Logic and Computation},
year = {2018},
doi = {10.1093/logcom/exy003},
author = {Emanuele Frittaion and Pelupessy, Florian and Silvia Steila and Keita Yokoyama}
}
@article {1812,
title = {Truncation and Semi-Decidability Notions in Applicative Theories},
journal = {The Journal of Symbolic Logic},
volume = {83},
year = {2018},
pages = {967-990},
abstract = {BON+ is an applicative theory and closely related to the first order parts of
the standard systems of explicit mathematics. As such it is also a natural framework
for abstract computations. In this article we analyze this aspect of BON+ more closely.
First a point is made for introducing a new operation τN , called truncation, to obtain a
natural formalization of partial recursive functions in our applicative framework. Then we
introduce the operational versions of a series of notions that are all equivalent to semi-
decidability in ordinary recursion theory on the natural numbers, and study their mutual
relationships over BON+ with τN .},
doi = {10.7892/boris.125568},
url = {http://www.iam.unibe.ch/ltgpub/2016/jarosa16.pdf},
author = {Gerhard J{\"a}ger and Timtej Rosebrock and Kentaro Sato}
}
@inbook {1779,
title = {Unfolding schematic systems},
booktitle = {Feferman on Foundations - Logic, Mathematics, Philosophy},
year = {2018},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2016/str16.pdf},
author = {Thomas Strahm},
editor = {Gerhard J{\"a}ger and Wilfried Sieg}
}
@inbook {1852,
title = {A First-Order Logic for Reasoning About Higher-Order Upper and Lower Probabilities},
booktitle = {Symbolic and Quantitative Approaches to Reasoning with Uncertainty: 14th European Conference, ECSQARU 2017, Lugano, Switzerland, July 10{\textendash}14, 2017, Proceedings},
year = {2017},
pages = {491-500},
publisher = {Springer International Publishing},
organization = {Springer International Publishing},
address = {Cham},
isbn = {978-3-319-61581-3},
url = {http://www.iam.unibe.ch/ltgpub/2017/sdo17a.pdf},
author = {Nenad Savi{\'c} and Dragan Doder and Ognjanovi{\'c}, Zoran},
editor = {Antonucci, Alessandro and Cholvy, Laurence and Papini, Odile}
}
@article {1880,
title = {A modular ordinal analysis of metapredicative subsystems of second order arithmetic},
year = {2017},
url = {http://www.iam.unibe.ch/ltgpub/2017/pro17.pdf},
author = {Dieter Probst}
}
@article {1848,
title = {Contributions to Intuitionistic Epistemic Logic},
year = {2017},
month = {April},
publisher = {Institute of Computer Science},
isbn = {978-1-326-98481-6},
url = {http://www.iam.unibe.ch/ltgpub/2017/mar17.pdf},
author = {Michel Marti}
}
@article {marti-metcalfe16,
title = {Expressivity in Chain-Based Modal Logics},
journal = {Archive for Mathematical Logic},
volume = {57},
year = {2017},
pages = {361-380},
url = {http://www.iam.unibe.ch/ltgpub/2017/mame17.pdf},
author = {Michel Marti and George Metcalfe}
}
@book {1900,
title = {Feferman on Foundations: Logic, Mathematics, Philosophy},
series = {Outstanding Contributions to Logic},
number = {13},
year = {2017},
publisher = {Springer International Publishing},
organization = {Springer International Publishing},
isbn = {9783319633329},
editor = {J{\"a}ger, G. and Sieg, W.}
}
@article {1895,
title = {Generic Large Cardinals and Systems of Filters},
journal = {The Journal of Symbolic Logic},
volume = {82},
year = {2017},
pages = {860-892},
doi = {10.1017/jsl.2017.27},
url = {http://www.iam.unibe.ch/ltgpub/2017/as17.pdf},
author = {Giorgio Audrito and Silvia Steila}
}
@proceedings {1854,
title = {Justification Logic with approximate conditional probabilities},
journal = { 6th international conference on Logic, Rationality and Interaction, LORI VI},
volume = {LORI 2017: Logic, Rationality, and Interaction},
year = {2017},
pages = {681-686},
publisher = {Springer},
address = {Hokkaido University, Sapporo, Japan},
url = {http://www.iam.unibe.ch/ltgpub/2017/oss17.pdf},
author = {Zoran Ognjanovi{\'c} and Nenad Savi{\'c} and Thomas Studer}
}
@article {1853,
title = {Logics with lower and upper probability operators},
journal = {International Journal of Approximate Reasoning},
volume = {88},
year = {2017},
pages = {148-168},
issn = {0888-613X},
url = {http://www.iam.unibe.ch/ltgpub/2017/sdo17b.pdf},
author = {Nenad Savi{\'c} and Dragan Doder and Zoran Ognjanovi{\'c}}
}
@article {ste16,
title = {Ramsey{\textquoteright}s Theorem for Pairs and k Colors as a Sub-Classical Principle of Arithmetic},
journal = {Journal of Symbolic Logic},
volume = {82},
year = {2017},
pages = {737-753},
url = {http://www.iam.unibe.ch/ltgpub/2016/best16.pdf},
author = {Berardi, S. and Silvia Steila}
}
@conference {1849,
title = {Temporal Justification Logic},
booktitle = {Proceedings of the Ninth Workshop on Methods for Modalities, Indian Institute of Technology, Kanpur, India, 8th to 10th January 2017},
year = {2017},
pages = {59-74},
publisher = {Open Publishing Association},
organization = {Open Publishing Association},
url = {http://www.iam.unibe.ch/ltgpub/2017/bgs17.pdf},
author = {Samuel Bucheli and Ghari, Meghdad and Thomas Studer},
editor = {Ghosh, Sujata and Ramanujam, R.}
}
@conference {1847,
title = {The Strength of the SCT Criterion},
booktitle = {Theory and Applications of Models of Computation - 14th Annual Conference, TAMC 2017, Bern, Switzerland, April 20-22, 2017, Proceedings},
year = {2017},
pages = {260-273},
doi = {10.1007/978-3-319-55911-7_19},
url = {http://www.iam.unibe.ch/ltgpub/2017/fsy17.pdf},
author = {Emanuele Frittaion and Silvia Steila and Keita Yokoyama},
editor = {T. V. Gopal and Gerhard J{\"a}ger and Silvia Steila}
}
@book {1851,
title = {Theory and Applications of Models of Computation TAMC 2017},
series = {Lecture Notes in Computer Science},
volume = {10185},
year = {2017},
publisher = {Springer International Publishing},
organization = {Springer International Publishing},
address = {Cham},
url = {http://boris.unibe.ch/104849/},
editor = {T.V. Gopal and Gerhard J{\"a}ger and Silvia Steila}
}
@conference {1777,
title = {A canonical model construction for intuitionistic distributed knowledge},
booktitle = {Advances in Modal Logic 2016},
year = {2016},
publisher = {College Publications},
organization = {College Publications},
url = {http://www.iam.unibe.ch/ltgpub/2016/jmidk16.pdf},
author = {Gerhard J{\"a}ger and Michel Marti},
editor = {Lev Beklemishev and S. Demri and A. M{\'a}t{\'e}}
}
@book {1797,
title = {Advances in Proof Theory},
series = {Progress in Computer Science and Applied Logic},
number = {28},
year = {2016},
publisher = {Birkh{\"a}user},
organization = {Birkh{\"a}user},
isbn = {978-3-319-29196-3},
editor = {Reinhard Kahle and Thomas Strahm and Thomas Studer}
}
@book {probst2016concepts,
title = {Concepts of Proof in Mathematics, Philosophy, and Computer Science},
series = {Ontos Mathematical Logic},
year = {2016},
publisher = {Walter De Gruyter Incorporated},
organization = {Walter De Gruyter Incorporated},
isbn = {9781501510809},
editor = {Dieter Probst and Peter Schuster}
}
@conference { kost16,
title = {Cyclic Proofs for Linear Temporal Logic},
booktitle = {Concepts of Proof in Mathematics, Philosophy, and Computer Science},
series = {Ontos Mathematical Logic},
volume = {6},
year = {2016},
publisher = {De Gruyter},
organization = {De Gruyter},
isbn = {978-1-5015-0262-0},
url = {http://www.iam.unibe.ch/ltgpub/2016/ks16.pdf},
author = {Ioannis Kokkinis and Thomas Studer},
editor = {Dieter Probst and Peter Schuster}
}
@article {1731,
title = {Intuitionistic common knowledge or belief},
journal = {Journal of Applied Logic},
volume = {18},
year = {2016},
chapter = {150},
abstract = {Starting off from the usual language of modal logic for multi-agent systems dealing with the agents{\textquoteright} knowledge/belief and common knowledge/belief we define so-called epistemic Kripke structures for intuitionistic (common) knowledge/belief. Then we introduce corresponding deductive systems and show that they are sound and complete with respect to these semantics.},
keywords = {Canonical models, Common knowledge, Intuitionistic modal logic},
doi = {10.7892/boris.71315},
url = {http://www.iam.unibe.ch/ltgpub/2015/jmick15.pdf},
author = {Gerhard J{\"a}ger and Michel Marti}
}
@article {1783,
title = {Intuitionistic modal logic made explicit},
journal = {IfCoLog Journal of Logics and their Applications},
volume = {3},
year = {2016},
pages = {877-901},
url = {http://www.iam.unibe.ch/ltgpub/2016/mast16.pdf},
author = {Michel Marti and Thomas Studer}
}
@article {1817,
title = {Justification with Nominals},
year = {2016},
isbn = {978-1-326-85065-4},
doi = {10.7892/boris.92524},
url = {http://www.iam.unibe.ch/ltgpub/2016/kas16.pdf},
author = {Alexander Kashev}
}
@conference { koogst16,
title = {Probabilistic Justification Logic},
booktitle = {Symposium on Logical Foundations in Computer Science 2016},
year = {2016},
publisher = {Springer},
organization = {Springer},
doi = {10.7892/boris.79976},
url = {http://www.iam.unibe.ch/ltgpub/2016/kos16.pdf},
author = {Ioannis Kokkinis and Zoran Ognjanovi{\'c} and Thomas Studer},
editor = {Sergei Artemov and Nerode, Anil}
}
@book {1796,
title = {Relationale Datenbanken: Von den theoretischen Grundlagen zu Anwendungen mit PostgreSQL},
series = {eXamen.press},
year = {2016},
publisher = {Springer Berlin Heidelberg},
organization = {Springer Berlin Heidelberg},
isbn = {9783662465714},
url = {http://db-buch.inf.unibe.ch},
author = {Thomas Studer}
}
@article {1753,
title = {Relativizing operational set theory},
journal = {The Bulletin of Symbolic Logic},
volume = {22},
year = {2016},
month = {09},
pages = {332-352},
abstract = {We introduce a way of relativizing operational set theory that also
takes care of application. After presenting the basic approach and
proving some essential properties of this new form of relativization we
turn to the notion of relativized regularity and to the system OST(LR)
that extends OST by a limit axiom claiming that any set is element
of a relativized regular set. Finally we show that OST(LR) is proof-
theoretically equivalent to the well-known theory KPi for a recursively
inaccessible universe.
},
issn = {1079-8986},
url = {http://www.iam.unibe.ch/ltgpub/2015/jae15.pdf},
author = {Gerhard J{\"a}ger}
}
@article {1792,
title = {Reverse mathematical bounds for the Termination Theorem},
journal = {Annals of Pure and Applied Logic},
year = {2016},
abstract = {Abstract In 2004 Podelski and Rybalchenko expressed the termination of transition-based programs as a property of well-founded relations. The classical proof by Podelski and Rybalchenko requires Ramsey{\textquoteright}s Theorem for pairs which is a purely classical result, therefore extracting bounds from the original proof is non-trivial task. Our goal is to investigate the termination analysis from the point of view of Reverse Mathematics. By studying the strength of Podelski and Rybalchenko{\textquoteright}s Termination Theorem we can extract some information about termination bounds.},
issn = {0168-0072},
doi = {10.1016/j.apal.2016.06.001},
url = {http://www.iam.unibe.ch/ltgpub/2016/styo16.pdf},
author = {Silvia Steila and Keita Yokoyama}
}
@conference { kok16,
title = {The Complexity of Non-Iterated Probabilistic Justification Logic},
booktitle = {Foundations of Information and Knowledge Systems -- FoIKS 2016},
year = {2016},
publisher = {Springer},
organization = {Springer},
doi = {10.7892/boris.79973},
url = {http://www.iam.unibe.ch/ltgpub/2016/kok16.pdf},
author = {Ioannis Kokkinis},
editor = {Simari, Guillermo and Gyssens, Marc}
}
@inbook {bjs15,
title = {Theories of proof-theoretic strength $\psi$($\Gamma_{\Omega+1}$)},
booktitle = {Concepts of Proof in Mathematics, Philosophy, and Computer Science},
series = {Ontos Mathematical Logic},
volume = {6},
year = {2016},
month = {January},
publisher = {De Gruyter},
organization = {De Gruyter},
isbn = {978-1-5015-0263-7},
url = {http://www.iam.unibe.ch/ltgpub/2015/bjs15.pdf},
author = {Ulrik Torben Buchholtz and Gerhard J{\"a}ger and Thomas Strahm},
editor = {Dieter Probst and Peter Schuster}
}
@article {1793,
title = {Uncertain Reasoning in Justification Logic},
year = {2016},
publisher = {University of Bern},
type = {phd},
address = {Switzerland},
url = {http://www.iam.unibe.ch/ltgpub/2016/kokphd16.pdf},
author = {Ioannis Kokkinis}
}
@article {Kuznets01062016,
title = {Weak arithmetical interpretations for the Logic of Proofs},
journal = {Logic Journal of IGPL},
volume = {24},
number = {3},
year = {2016},
pages = {424-440},
abstract = {Artemov established an arithmetical interpretation for the Logics of Proofs LPCS, which yields a classical provability semantics for the modal logic S4. The Logics of Proofs are parameterized by so-called constant specifications CS, stating which axioms can be used in the reasoning process, and the arithmetical interpretation relies on constant specifications being finite. In this article, we remove this restriction by introducing weak arithmetical interpretations that are sound and complete for a wide class of constant specifications, including infinite ones. In particular, they interpret the full Logic of Proofs LP.},
url = {http://www.iam.unibe.ch/ltgpub/2016/kust16.pdf},
author = {Roman Kuznets and Thomas Studer}
}
@article {sat15b,
title = {A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman{\textquoteright}s explicit mathematics T0},
journal = {Annals of pure and applied logic},
volume = {166},
number = {7-8},
year = {2015},
pages = {800-835},
publisher = {Elsevier},
abstract = {We partially solve a long-standing problem in the proof theory of explicit mathematics or the proof theory in general. Namely, we give a lower bound of Feferman?s system T0 of explicit mathematics (but only when formulated on classical logic) with a concrete interpretat ion of the subsystem {$Σ$}12-AC+ (BI) of second order arithmetic inside T0. Whereas a lower bound proof in the sense of proof-theoretic reducibility or of ordinalanalysis was already given in 80s, the lower bound in the sense of interpretability we give here is new. We apply the new interpretation method developed by the author and Zumbrunnen (2015), which can be seen as the third kind of model construction method for classical theories, after Cohen?s forcing and Krivine?s classical realizability. It gives us an interpretation between classical theories, by composing interpretations between intuitionistic theories.},
url = {http://www.iam.unibe.ch/ltgpub/2015/sat15b.pdf},
author = {Kentaro Sato}
}
@article {sz14,
title = {A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP},
journal = {Annals of pure and applied logic},
volume = {166},
number = {2},
year = {2015},
pages = {121-186},
publisher = {Elsevier},
abstract = {We introduce a version of operational set theory, OST?, without a choice operation, which has a machinery for {$Δ$}0{$Δ$}0 separation based on truth functions and the separation operator, and a new kind of applicative set theory, so-called weak explicit set theory WEST, based on G{\"o}del operations. We show that both the theories and Kripke?Platek set theory KPKP with infinity are pairwise {$\Pi$}1{$\Pi$}1 equivalent. We also show analogous assertions for subtheories with ?-induction restricted in various ways and for supertheories extended by powerset, beta, limit and Mahlo operations. Whereas the upper bound is given by a refinement of inductive definition in KPKP, the lower bound is by a combination, in a specific way, of realisability, (intuitionistic) forcing and negative interpretations. Thus, despite interpretability between classical theories, we make ?a detour via intuitionistic theories?. The combined interpretation, seen as a model construction in the sense of Visser{\textquoteright}s miniature model theory, is a new way of construction for classical theories and could be said the third kind of model construction ever used which is non-trivial on the logical connective level, after generic extension {\`a} la Cohen and Krivine{\textquoteright}s classical realisability model.},
url = {http://www.iam.unibe.ch/ltgpub/2014/sz14.pdf},
author = {Kentaro Sato and Rico Zumbrunnen}
}
@inbook {jp13,
title = {A proof-theoretic analysis of theories for stratified inductive definitions},
booktitle = {Gentzen{\textquoteright}s Centenary: The Quest for Consistency},
year = {2015},
note = {2014},
publisher = {Springer},
organization = {Springer},
doi = {10.1007/978-3-319-10103-3},
url = {http://www.iam.unibe.ch/ltgpub/2013/jp13.pdf},
author = {Gerhard J{\"a}ger and Dieter Probst},
editor = {Reinhard Kahle and Michael Rathjen}
}
@article {ebat15,
title = {Applicative theories for logarithmic complexity classes},
journal = {Theoretical Computer Science},
volume = {585},
year = {2015},
month = {June},
pages = {115-135},
publisher = {Elsevier},
abstract = {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{\textquoteright}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{\textquoteright}s theories [6] formalising B.},
url = {http://www.iam.unibe.ch/ltgpub/2015/ebat15.pdf},
author = {Sebastian Eberhard}
}
@article {wer15,
title = {Controlled Query Evaluation in General Semantics with Incomplete Information},
year = {2015},
note = {ISBN 978-1-326-21681-8},
month = {March},
publisher = {Institut f{\"u}r Informatik und angewandte Mathematik},
type = {phd},
url = {http://www.iam.unibe.ch/ltgpub/2015/wer15.pdf},
author = {Johannes Werner}
}
@article {kmos15,
title = {First steps towards probabilistic justification logic},
journal = {Logic Journal of IGPL},
volume = {23},
number = {4},
year = {2015},
month = {June},
pages = {662-687},
publisher = {Oxford University Press},
abstract = {In this article, we introduce the probabilistic justification logic PJ, a logic in which we can reason about the probability of justification statements. We present its syntax and semantics, and establish a strong completeness theorem. Moreover, we investigate the relationship between PJ and the logic of uncertain justifications.},
url = {http://www.iam.unibe.ch/ltgpub/2015/kmos15.pdf},
author = {Ioannis Kokkinis and Petar Maksimovi{\'c} and Zoran Ognjanovi{\'c} and Thomas Studer}
}
@article {1756,
title = {From a Flexible Type System to Metapredicative Wellordering Proofs},
year = {2015},
url = {http://www.iam.unibe.ch/ltgpub/2015/ran15.pdf},
author = {Ranzi, Florian}
}
@article {sat15a,
title = {Full and hat inductive definitions are equivalent in NBG},
journal = {Archive for Mathematical Logic},
volume = {54},
number = {1-2},
year = {2015},
pages = {75-112},
publisher = {Springer},
abstract = {A new research project has, quite recently, been launched to clarify how different, from systems in second order number theory extending ACA 0, those in second order set theory extending NBG (as well as those in n + 3-th order number theory extending the so-called Bernays?G{\"o}del expansion of full n + 2-order number theory etc.) are. In this article, we establish the equivalence between {$Δ$}10{$\backslash$}bf-LFP and {$Δ$}10{$\backslash$}bf-FP, which assert the existence of a least and of a (not necessarily least) fixed point, respectively, for positive elementary operators (or between {$Δ$}n+20{$\backslash$}bf-LFP and {$Δ$}n+20{$\backslash$}bf-FP). Our proof also shows the equivalence between ID 1 and {\^{ }}ID1, both of which are defined in the standard way but with the starting theory PA replaced by ZFC (or full n + 2-th order number theory with global well-ordering).},
url = {http://www.iam.unibe.ch/ltgpub/2015/sat15a.pdf},
author = {Kentaro Sato}
}
@article {fkm15,
title = {Modal interpolation via nested sequents},
journal = {Annals of pure and applied logic},
volume = {166},
number = {3},
year = {2015},
month = {March},
pages = {274-305},
publisher = {Elsevier},
abstract = {The main method of proving the Craig Interpolation Property (CIP) constructively uses cut-free sequent proof systems. Until now, however, no such method has been known for proving the CIP using more general sequent-like proof formalisms, such as hypersequents, nested sequents, and labelled sequents. In this paper, we start closing this gap by presenting an algorithm for proving the CIP for modal logics by induction on a nested-sequent derivation. This algorithm is applied to all the logics of the so-called modal cube.},
url = {http://www.iam.unibe.ch/ltgpub/2015/fkm15.pdf},
author = {Melvin Fitting and Roman Kuznets}
}
@article {1773,
title = {Soundness and completeness of a first order probabilistic logic with approximate conditional probabilities},
year = {2015},
url = {http://www.iam.unibe.ch/ltgpub/2016/mat16.pdf},
author = {Stephan Matter}
}
@book {1778,
title = {Turing{\textquoteright}s Revolution: The Impact of His Ideas about Computability},
year = {2015},
pages = {329},
publisher = {Birkh{\"a}user},
organization = {Birkh{\"a}user},
url = {http://www.springer.com/de/book/9783319221557},
author = {Giovanni Sommaruga and Thomas Strahm}
}
@inbook {esu15,
title = {Unfolding Feasible Arithmetic and Weak Truth},
booktitle = {Unifying the Philosophy of Truth},
series = {Logic, Epistemology, and the Unity of Science},
volume = {36},
year = {2015},
pages = {153-167},
publisher = {Springer Netherlands},
organization = {Springer Netherlands},
address = {Dordrecht},
abstract = {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).},
url = {http://www.iam.unibe.ch/ltgpub/2015/esu15.pdf},
author = {Sebastian Eberhard and Thomas Strahm},
editor = {Theodora Achourioti and Henri Galinon and Jos{\'e} Mart{\'\i}nez Fern{\'a}ndez and Kentaro Fujimoto}
}
@article {ebe12a,
title = {A feasible theory of truth over combinatory algebra},
journal = {Annals of Pure and Applied Logic},
volume = {165},
number = {5},
year = {2014},
pages = {1009-1033},
keywords = {Truth theories},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.12.002},
url = {http://www.iam.unibe.ch/ltgpub/2012/ebe12a.pdf},
author = {Sebastian Eberhard}
}
@conference {mm14,
title = {A Hennessy-Milner Property for Many-Valued Modal Logics},
booktitle = {Advances in Modal Logic},
volume = {10},
year = {2014},
pages = {407-420},
publisher = {College Publications},
organization = {College Publications},
url = {http://www.iam.unibe.ch/ltgpub/2014/mm14.pdf},
author = {Michel Marti and George Metcalfe},
editor = {Rajeev Gor{\'e} and Barteld Kooi and Agi Kurucz}
}
@article {rs13,
title = {A note on the theory $\mathsf{SID}_{{<}\omega}$ of stratified induction},
journal = {Mathematical Logic Quarterly},
volume = {60},
number = {6},
year = {2014},
pages = {487-497},
issn = {1521-3870},
doi = {10.1002/malq.201300063},
url = {http://www.iam.unibe.ch/ltgpub/2013/rs13.pdf},
author = {Ranzi, Florian and Thomas Strahm}
}
@article {sw14,
title = {Censors for Boolean Description Logic},
journal = {Transactions on Data Privacy},
volume = {7},
year = {2014},
pages = {223-252},
issn = {1888-5063},
url = {http://www.iam.unibe.ch/ltgpub/2014/sw14.pdf},
author = {Thomas Studer and Johannes Werner}
}
@article {jz14,
title = {Explicit mathematics and operational set theory: some ontological comparisons},
journal = {The Bulletin of Symbolic Logic},
volume = {20},
year = {2014},
month = {9},
pages = {275-292},
issn = {1943-5894},
doi = {10.1017/bsl.2014.21},
url = {http://www.iam.unibe.ch/ltgpub/2014/jz14.pdf},
author = {Gerhard J{\"a}ger and Rico Zumbrunnen}
}
@article {sat14,
title = {Forcing for Hat Inductive Definitions in Arithmetic {\textendash} One of the Simplest Applications of Forcing {\textendash}},
journal = {Mathematical Logic Quarterly},
volume = {60},
number = {4-5},
year = {2014},
pages = {314-318},
abstract = {By forcing, we give a direct interpretation of $\widehat{\mathsf{ID}}_\omega$ into Avigad{\textquoteright}s $\mathsf{FP}$. To the best of the author{\textquoteright}s knowledge, this is one of the simplest applications of forcing to {\textquoteleft}{\textquoteleft}real problems{\textquoteright}{\textquoteright}.},
issn = {1521-3870},
doi = {10.1002/malq.201300044},
url = {http://www.iam.unibe.ch/ltgpub/2014/sat14.pdf},
author = {Kentaro Sato}
}
@article {fs14,
title = {From hierarchies to well-foundedness},
journal = {Archive for Mathematical Logic},
volume = {53},
number = {7{\textendash}8},
year = {2014},
publisher = {Springer Berlin Heidelberg},
issn = {0933-5846},
doi = {10.1007/s00153-014-0392-9},
url = {http://www.iam.unibe.ch/ltgpub/2014/fs14.pdf},
author = {Dandolo Flumini and Kentaro Sato}
}
@article {aks14,
title = {Justifying induction on modal $μ$-formulae},
journal = {Logic Journal of IGPL},
volume = {22},
year = {2014},
pages = {805-817},
abstract = {We define a rank function for formulae of the propositional modal $\mu$-calculus such that the rank of a fixed point is strictly bigger than the rank of any of its finite approximations. A rank function of this kind is needed, for instance, to establish the collapse of the modal $\mu$-hierarchy over transitive transition systems. We show that the range of the rank function is $\omega^\omega$. Further we establish that the rank is computable by primitive recursion, which gives us a uniform method to generate formulae of arbitrary rank below $\omega^\omega$.},
doi = {10.1093/jigpal/jzu001},
url = {http://www.iam.unibe.ch/ltgpub/2014/aks14.pdf},
author = {Alberucci, Luca and Kr{\"a}henb{\"u}hl, J{\"u}rg and Thomas Studer}
}
@article {ak13,
title = {Logical Omniscience As Infeasibility},
journal = {Annals of Pure and Applied Logic},
volume = {165},
number = {1},
year = {2014},
pages = {6-25},
abstract = {Abstract Logical theories for representing knowledge are often plagued by the so-called Logical Omniscience Problem. The problem stems from the clash between the desire to model rational agents, which should be capable of simple logical inferences, and the fact that any logical inference, however complex, almost inevitably consists of inference steps that are simple enough. This contradiction points to the fruitlessness of trying to solve the Logical Omniscience Problem qualitatively if the rationality of agents is to be maintained. We provide a quantitative solution to the problem compatible with the two important facets of the reasoning agent: rationality and resource boundedness. More precisely, we provide a test for the logical omniscience problem in a given formal theory of knowledge. The quantitative measures we use are inspired by the complexity theory. We illustrate our framework with a number of examples ranging from the traditional implicit representation of knowledge in modal logic to the language of justification logic, which is capable of spelling out the internal inference process. We use these examples to divide representations of knowledge into logically omniscient and not logically omniscient, thus trying to determine how much information about the reasoning process needs to be present in a theory to avoid logical omniscience.},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.07.003},
url = {http://www.iam.unibe.ch/ltgpub/2013/ak13.pdf},
author = {Sergei Artemov and Roman Kuznets}
}
@article {sav13a,
title = {Proof Internalization for Generalized Frege Systems for Classical Logic},
journal = {Annals of Pure and Applied Logic},
volume = {165},
number = {1},
year = {2014},
pages = {340-356},
abstract = {Abstract We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.07.017},
url = {http://www.iam.unibe.ch/ltgpub/2013/sav13a.pdf},
author = {Yury Savateev}
}
@article {bks12a,
title = {Realizing Public Announcements by Justifications},
journal = {Journal of Computer and System Sciences},
volume = {80},
number = {6},
year = {2014},
pages = {1046-1066},
abstract = {Modal public announcement logics study how beliefs change after public announcements. However, these logics cannot express the reason for a new belief. Justification logics fill this gap since they can formally represent evidence and justifications for an agent{\textquoteright}s belief. We present ${\sf OPAL(K)}$ and ${\sf JPAL(K)}$, two alternative justification counterparts of Gerbrandy{\textendash}Groeneveld{\textquoteright}s public announcement logic ${\sf PAL(K)}$. We show that ${\sf PAL(K)}$ is the forgetful projection of both ${\sf OPAL(K)}$ and ${\sf JPAL(K)}$. We also establish that ${\sf JPAL(K)}$ partially realizes ${\sf PAL(K)}$. The question whether a similar result holds for ${\sf OPAL(K)}$ is still open.},
keywords = {Belief revision, Dynamic epistemic logic, justification logic, Public announcements},
doi = {10.1016/j.jcss.2014.04.001},
url = {http://www.iam.unibe.ch/ltgpub/2012/bks12a.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer}
}
@article {sat12,
title = {Relative predicativity and dependent recursion in second-order set theory and higher-order theories},
journal = {The Journal of Symbolic Logic},
volume = {79},
year = {2014},
month = {9},
pages = {712-732},
issn = {1943-5886},
doi = {10.1017/jsl.2014.28},
url = {http://www.iam.unibe.ch/ltgpub/2012/sat12.pdf},
author = {Kentaro Sato}
}
@article {stu12b,
title = {A Universal Approach to Guarantee Data Privacy},
journal = {Logica Universalis},
volume = {7},
number = {2},
year = {2013},
pages = {195-209},
url = {http://www.iam.unibe.ch/ltgpub/2012/stu12b.pdf},
author = {Thomas Studer}
}
@article {mck12a,
title = {Canonical proof nets for classical logic},
journal = {Annals of Pure and Applied Logic},
volume = {164},
number = {6},
year = {2013},
pages = {702-732},
issn = {0168-0072},
doi = {10.1016/j.apal.2012.05.007},
url = {http://www.iam.unibe.ch/ltgpub/2012/mck12a.pdf},
author = {Richard McKinley}
}
@article {zum13,
title = {Contributions to Operational Set Theory},
year = {2013},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2013/zum13.pdf},
author = {Rico Zumbrunnen}
}
@inbook {bks13,
title = {Decidability for Justification Logics Revisited},
booktitle = {Logic, Language, and Computation, 9th~International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC~2011, Kutaisi, Georgia, September 26-30, 2011, Revised Selected Papers},
volume = {7758},
year = {2013},
pages = {166-181},
publisher = {Springer},
organization = {Springer},
abstract = {Justification logics are propositional modal-like logics that instead of statements \emph{$A$~is known} include statements of the form \emph{$A$~is known for reason~$t$} where the term~$t$ can represent an informal justification for~$A$ or a formal proof of~$A$. In our present work, we introduce model-theoretic tools, namely: filtrations and a certain form of generated submodels, in the context of justification logic in order to obtain decidability results. Apart from reproving already known results in a uniform way, we also prove new results. In particular, we use our submodel construction to establish decidability for a justification logic with common knowledge for which so far no decidability proof was available.},
keywords = {decidability, filtration, justification logic},
doi = {10.1007/978-3-642-36976-6_12},
url = {http://www.iam.unibe.ch/ltgpub/2013/bks13.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Guram Bezhanishvili and Sebastian L{\"o}bner and Vincenzo Marra and Frank Richter}
}
@article {stu13,
title = {Decidability for some justification logics with negative introspection},
journal = {The Journal of Symbolic Logic},
volume = {78},
number = {2},
year = {2013},
pages = {388-402},
url = {http://www.iam.unibe.ch/ltgpub/2013/stu13.pdf},
author = {Thomas Studer}
}
@article {jae13,
title = {Operational closure and stability},
journal = {Annals of Pure and Applied Logic},
volume = {164},
number = {7{\textendash}8},
year = {2013},
pages = {813-821},
abstract = {In this article we introduce and study the notion of operational closure: a transitive set d is called operationally closed iff it contains all constants of $\mathsf{OST}$ and any operation $f\in d$ applied to an element $a\in d$ yields an element $fa\in d$ , provided that $f$ applied to a has a value at all. We will show that there is a direct relationship between operational closure and stability in the sense that operationally closed sets behave like $\Sigma_1$ substructures of the universe. This leads to our final result that $\mathsf{OST}$ plus the axiom $(\mathsf{OLim})$ , claiming that any set is element of an operationally closed set, is proof-theoretically equivalent to the system $\mathsf{KP}+(\Sigma_1\text{-}\mathsf{Sep})$ of Kripke-Platek set theory with infinity and $\Sigma_1$ separation. We also characterize the system $\mathsf{OST}$ plus the existence of one operationally closed set in terms of Kripke-Platek set theory with infinity and a parameter-free version of $\Sigma_1$ separation.},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.01.004},
url = {http://www.iam.unibe.ch/ltgpub/2013/jae13.pdf},
author = {Gerhard J{\"a}ger}
}
@article {mck12b,
title = {Proof Nets for Herbrand{\textquoteright}s Theorem},
journal = {ACM Transactions on Computational Logic},
volume = {14},
number = {1},
year = {2013},
pages = {5},
doi = {10.1145/2422085.2422090},
url = {http://www.iam.unibe.ch/ltgpub/2012/mck12b.pdf},
author = {Richard McKinley}
}
@article {bra13,
title = {Proof Search in Propositional Circumscription and Default Logic},
year = {2013},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2013/bra13.pdf},
author = {Brambilla, Peppo}
}
@inbook {ks13,
title = {Update as Evidence: Belief Expansion},
booktitle = {Logical Foundations of Computer Science, International Symposium, LFCS~2013, San Diego, CA, USA, January 6{\textendash}8, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7734},
year = {2013},
pages = {266-279},
publisher = {Springer},
organization = {Springer},
abstract = {We introduce a justification logic with a novel constructor for evidence terms, according to which the new information itself serves as evidence for believing it. We provide a sound and complete axiomatization for belief expansion and minimal change and explain how the minimality can be graded according to the strength of reasoning. We also provide an evidential analog of the Ramsey axiom.},
doi = {10.1007/978-3-642-35722-0_19},
url = {http://www.iam.unibe.ch/ltgpub/2013/ks13.pdf},
author = {Roman Kuznets and Thomas Studer},
editor = {Sergei Artemov and Nerode, Anil}
}
@article {ebe13,
title = {Weak applicative theories, truth, and computational complexity},
year = {2013},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2013/ebe13.pdf},
author = {Sebastian Eberhard}
}
@article {flu13,
title = {Weak well orders},
year = {2013},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2013/flu13.pdf},
author = {Dandolo Flumini}
}
@conference {1307,
title = {About the Strength of Operational Regularity},
booktitle = {Logic, Construction, Computation},
year = {2012},
pages = {305-324},
publisher = {Ontos Verlag},
organization = {Ontos Verlag},
url = {http://www.iam.unibe.ch/ltgpub/2012/jz12.pdf},
author = {Gerhard J{\"a}ger and Rico Zumbrunnen},
editor = {Ulrich Berger and Hannes Diener and Peter Schuster and Monika Seisenberger}
}
@conference {ms12,
title = {Cut-elimination for the mu-calculus with one variable},
booktitle = {Fixed Points in Computer Science 2012},
series = {EPTCS},
volume = {77},
year = {2012},
pages = {47-54},
publisher = {Open Publishing Association},
organization = {Open Publishing Association},
url = {http://www.iam.unibe.ch/ltgpub/2012/ms12.pdf},
author = {Grigori Mints and Thomas Studer}
}
@article {1309,
title = {Java-Programm zur interaktiven Bearbeitung von JALC-Herleitungen},
year = {2012},
publisher = {Universit{\"a}t Bern},
type = {Bachelor{\textquoteright}s Thesis},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2012/koh12.pdf},
author = {Kohler, Roger Peter}
}
@article {1310,
title = {Justification Logics with Common Knowledge},
year = {2012},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2012/buc12.pdf},
author = {Samuel Bucheli}
}
@conference {1311,
title = {Justifications, Ontology, and Conservativity},
booktitle = {Advances in Modal Logic, volume 9},
year = {2012},
pages = {437-458},
publisher = {College Publications},
organization = {College Publications},
url = {http://www.iam.unibe.ch/ltgpub/2012/ks12.pdf},
author = {Roman Kuznets and Thomas Studer},
editor = {Thomas Bolander and Torben Bra{\"u}ner and Silvio Ghilardi and Lawrence Moss}
}
@conference {1312,
title = {Justified Terminological Reasoning},
booktitle = {Proceedings of Perspectives of System Informatics PSI{\textquoteright}11},
series = {Lecture Notes in Computer Science},
volume = {7162},
year = {2012},
pages = {349-361},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2012/stu12.pdf},
author = {Thomas Studer},
editor = {E. Clarke and I. Virbitskaite and A Voronkov}
}
@article {1313,
title = {Lower complexity bounds in justification logic},
journal = {Annals of Pure and Applied Logic},
volume = {163},
year = {2012},
note = {Published online November~2011},
pages = {888-905},
abstract = {Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in~NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound. The proof method is then extended to provide a uniform proof that the corresponding full pure justification logics are $\Pi^p_2$-hard, reproving and generalizing an earlier result by Milnikel.},
keywords = {Logic of Proofs},
doi = {10.1016/j.apal.2011.09.010},
url = {http://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/APAL09_final.pdf},
author = {Buss, Samuel R. and Roman Kuznets}
}
@article {goe12,
title = {On the Realization and Classification of Justification Logics},
year = {2012},
publisher = {Universit{\"a}t Bern},
type = {phdphd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2012/goe12.pdf},
author = {Remo Goetschi}
}
@article {1314,
title = {Product-free Lambek calculus is NP-complete},
journal = {Annals of Pure and Applied Logic},
volume = {163},
year = {2012},
note = {The Symposium on Logical Foundations of Computer Science 2009},
pages = {775-788},
doi = {10.1016/j.apal.2011.09.017},
url = {http://www.iam.unibe.ch/ltgpub/2012/sav12.pdf},
author = {Yury Savateev}
}
@article {1306,
title = {Realization for Justification Logics via Nested Sequents: Modularity through Embedding},
journal = {Annals of Pure and Applied Logic},
volume = {163},
year = {2012},
month = {September},
pages = {1271-1298},
doi = {10.1016/j.apal.2012.02.002},
url = {http://www.iam.unibe.ch/ltgpub/2012/gk12.pdf},
author = {Remo Goetschi and Roman Kuznets}
}
@article {bs12,
title = {Syntactic cut-elimination for a fragment of the modal mu-calculus},
journal = {Annals of Pure and Applied Logic},
volume = {163},
number = {12},
year = {2012},
pages = {1838-1853},
url = {http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf},
author = {Kai Br{\"u}nnler and Thomas Studer}
}
@conference {1315,
title = {Weak theories of truth and explicit mathematics},
booktitle = {Logic, Construction, Computation},
year = {2012},
pages = {157-184},
publisher = {Ontos Verlag},
organization = {Ontos Verlag},
url = {http://www.iam.unibe.ch/ltgpub/2012/es12a.pdf},
author = {Sebastian Eberhard and Thomas Strahm},
editor = {Ulrich Berger and Hannes Diener and Peter Schuster and Monika Seisenberger}
}
@article {1319,
title = {A Buchholz rule for modal fixed point logics},
journal = {Logica Universalis},
volume = {5},
year = {2011},
note = {To appear, 2010},
pages = {1-19},
doi = {10.1007/s11787-010-0022-1},
url = {http://www.iam.unibe.ch/ltgpub/2011/js11.pdf},
author = {Gerhard J{\"a}ger and Thomas Studer}
}
@article {1317,
title = {Admissible closures of polynomial time computable arithmetic},
journal = {Archive for Mathematical Logic},
volume = {50},
year = {2011},
note = {Submitted, 2010},
pages = {643-660},
url = {http://www.iam.unibe.ch/ltgpub/2011/ps11.pdf},
author = {Dieter Probst and Thomas Strahm}
}
@conference {1318,
title = {An application of justification logic to protocol verification},
booktitle = {Proceedings of Computational Intelligence and Security CIS 2011},
year = {2011},
pages = {779-783},
publisher = {IEEE},
organization = {IEEE},
url = {http://www.iam.unibe.ch/ltgpub/2011/stu11b.pdf},
author = {Thomas Studer}
}
@article {1325,
title = {Applicative theories on tree ordinal numbers},
year = {2011},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2011/fab11.pdf},
author = {Daniel Fabian}
}
@article {1320,
title = {Justification Logic, Inference Tracking, and Data Privacy},
journal = {Logic and Logical Philosophy},
volume = {20},
year = {2011},
pages = {297-306},
url = {http://www.iam.unibe.ch/ltgpub/2011/stu11a.pdf},
author = {Thomas Studer}
}
@article {1321,
title = {Justifications for Common Knowledge},
journal = {Journal of Applied Non-classical Logics},
volume = {21},
year = {2011},
note = {To appear, 2011},
pages = {35-60},
doi = {10.3166/JANCL.21.35-60},
url = {http://www.iam.unibe.ch/ltgpub/2011/bks11a.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Valentin Goranko and Wojtek Jamroga}
}
@article {1326,
title = {On the Relationship between Choice Schemes and Iterated Class Comprehension in Set Theory},
year = {2011},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2011/kra11.pdf},
author = {Kr{\"a}henb{\"u}hl, J{\"u}rg}
}
@conference {1322,
title = {Partial Realization in Dynamic Justification Logic},
booktitle = {Logic, Language, Information and Computation, 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, 2011, Proceedings},
series = {Lecture Notes in Artificial Intelligence},
volume = {6642},
year = {2011},
pages = {35-51},
doi = {10.1007/978-3-642-20920-8_9},
url = {http://www.iam.unibe.ch/ltgpub/2011/bks11b.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Lev Beklemishev and de Queiroz, Ruy}
}
@article {1324,
title = {Realizability in weak systems of explicit mathematics},
journal = {Mathematical Logic Quarterly},
volume = {57},
year = {2011},
note = {To appear, 2010},
pages = {551-565},
url = {http://www.iam.unibe.ch/ltgpub/2011/ss11.pdf},
author = {Spescha, Daria and Thomas Strahm}
}
@article {sav13b,
title = {Sequent Calculus for Justifications},
journal = {Journal of Logic and Computation},
year = {2011},
note = {2013},
abstract = {We present a cut-free sequent calculus that can internalize its own
proofs, providing a new justification system for modal logic.
-------
TABLEAUX 2011
Workshops, Tutorials, and Short Papers
Martin Giese and Roman Kuznets (editors)
Technical Report IAM-11-002, 4{\textendash}8 July 2011
},
url = {http://www.iam.unibe.ch/ltgpub/2013/sav13b.pdf},
author = {Yury Savateev}
}
@article {1323,
title = {The provably terminating operations of the subsystem PETJ of explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {162},
year = {2011},
note = {Submitted, 2010},
pages = {934-947},
doi = {10.1016/j.apal.2011.04.004},
url = {http://www.iam.unibe.ch/ltgpub/2011/pro11.pdf},
author = {Dieter Probst}
}
@article {1316,
title = {The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories},
journal = {Annals of Pure and Applied logic},
volume = {162},
year = {2011},
month = {2011},
pages = {647-660},
keywords = {Suslin operator in applicative theories},
doi = {10.1016/j.apal.2011.01.009},
url = {http://www.iam.unibe.ch/ltgpub/2011/jp11.pdf},
author = {Gerhard J{\"a}ger and Dieter Probst}
}
@conference {1342,
title = {A Syntactic Realization Theorem for Justification Logics},
booktitle = {Advances in Modal Logic, Volume 8},
year = {2010},
pages = {39-58},
publisher = {College Publications},
organization = {College Publications},
abstract = {Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms~$\mathsf{d}$, $\mathsf{t}$, $\mathsf{b}$, $\mathsf{4}$, and~$\mathsf{5}$ with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting{\textquoteright}s realization merging technique. We further strengthen the realization theorem for $\mathsf{KB5}$~and~$\mathsf{S5}$ by showing that the positive introspection operator is superfluous.},
keywords = {realization theorem},
url = {http://www.iam.unibe.ch/ltgpub/2010/bgk10.pdf},
author = {Kai Br{\"u}nnler and Remo Goetschi and Roman Kuznets},
editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman}
}
@article {1330,
title = {Annotated Systems for Common Knowledge},
year = {2010},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2010/weh10.pdf},
author = {Wehbe, Ricardo}
}
@conference {1331,
title = {Expansion nets: Proof nets for for propositional classical logic},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 17)},
series = {Lecture Notes in Computer Science},
volume = {6397},
year = {2010},
note = {10.1007/978-3-642-16242-8_38},
pages = {535-549},
publisher = {Springer Berlin / Heidelberg},
organization = {Springer Berlin / Heidelberg},
url = {http://www.iam.unibe.ch/ltgpub/2010/mck10a.pdf},
author = {Richard McKinley},
editor = {Ferm{\"u}ller, Christian and A Voronkov}
}
@article {1327,
title = {Explicit Evidence Systems with Common Knowledge},
year = {2010},
month = {may},
publisher = {arXiv.org},
type = {E-print},
abstract = {Justification logics are epistemic logics that explicitly include justifications for the agents{\textquoteright} knowledge. We develop a multi-agent justification logic with evidence terms for individual agents as well as for common knowledge. We define a Kripke-style semantics that is similar to Fitting{\textquoteright}s semantics for the Logic of Proofs~$\mathsf{LP}$. We show the soundness, completeness, and finite model property of our multi-agent justification logic with respect to this Kripke-style semantics. We demonstrate that our logic is a conservative extension of Yavorskaya{\textquoteright}s minimal bimodal explicit evidence logic, which is a two-agent version of~$\mathsf{LP}$. We discuss the relationship of our logic to the multi-agent modal logic~$\mathsf{S4}$ with common knowledge. Finally, we give a brief analysis of the coordinated attack problem in the newly developed language of our logic.},
url = {http://arxiv.org/abs/1005.0484},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer}
}
@conference {1340,
title = {Justified Belief Change},
booktitle = {Proceedings of the Second ILCLI International Workshop on Logic and Philosphy of Knowledge, Communication and Action (LogKCA-10)},
year = {2010},
pages = {135-155},
publisher = {University of the Basque Country Press},
organization = {University of the Basque Country Press},
abstract = {Justification Logic is a framework for reasoning about evidence and justification. Public Announcement Logic is a framework for reasoning about belief changes caused by public announcements. This paper develops JPAL, a dynamic justification logic of public announcements that corresponds to the modal theory of public announcements due to Gerbrandy and Groeneveld. JPAL allows us to reason about evidence brought about by and changed by Gerbrandy{\textendash}Groeneveld-style public announcements.},
url = {http://www.iam.unibe.ch/ltgpub/2010/bkrss10.pdf},
author = {Samuel Bucheli and Roman Kuznets and Renne, Bryan and Sack, Joshua and Thomas Studer},
editor = {Arrazola, Xabier and Ponte, Mar\'{\i}a}
}
@conference {1332,
title = {Modal Fixed Point Logics},
booktitle = {Logics and Languages for Reliability and Security},
series = {NATO Science for Peace and Security Series - D: Information and Communication Security},
volume = {25},
year = {2010},
publisher = {IOS Press},
organization = {IOS Press},
doi = {10.3233/978-1-60750-100-8-129},
url = {http://www.iam.unibe.ch/ltgpub/2010/jae10.pdf},
author = {Gerhard J{\"a}ger},
editor = {J. Esparza and B. Spanfelner and O. Grumberg}
}
@article {1333,
title = {Nested Sequents},
year = {2010},
publisher = {Universit{\"a}t Bern},
type = {Habilitationsschrift},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://arxiv.org/abs/1004.1845v1},
author = {Kai Br{\"u}nnler}
}
@conference {1334,
title = {Privacy Preserving Modules for Ontologies},
booktitle = {Proceedings of Perspectives of System Informatics PSI{\textquoteright}09},
series = {Lecture Notes in Computer Science},
volume = {5947},
year = {2010},
pages = {380-387},
url = {http://www.iam.unibe.ch/ltgpub/2010/stu10a.pdf},
author = {Thomas Studer},
editor = {A. Pnueli and I. Virbitskaite and A Voronkov}
}
@article {1335,
title = {Proof-theoretic aspects of weak K{\"o}nig{\textquoteright}s Lemma},
year = {2010},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2010/bru10a.pdf},
author = {Brugger, Jon}
}
@article {1336,
title = {Proof-Theoretic Contributions to Modal Fixed Point Logics},
year = {2010},
publisher = {Universit{\"a}t Bern},
type = {Habilitationsschrift},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2010/stu10b.pdf},
author = {Thomas Studer}
}
@article {1328,
title = {Self-Referential Justifications in Epistemic Logic},
journal = {Theory of Computing Systems},
volume = {46},
year = {2010},
month = {may},
pages = {636-661},
abstract = {This paper is devoted to the study of self-referential proofs and/or justifications, i.e., valid proofs that prove statements about these same proofs. The goal is to investigate whether such self-referential justifications are present in the reasoning described by standard modal epistemic logics such as~$\mathsf{S4}$. We argue that the modal language by itself is too coarse to capture this concept of self-referentiality and that the language of justification logic can serve as an adequate refinement. We consider well-known modal logics of knowledge/belief and show, using explicit justifications, that~$\mathsf{S4}$, $\mathsf{D4}$, $\mathsf{K4}$, and~$\mathsf{T}$ with their respective justification counterparts~$\mathsf{LP}$, $\mathsf{JD4}$, $\mathsf{J4}$, and~$\mathsf{JT}$ describe knowledge that is self-referential in some strong sense. We also demonstrate that self-referentiality can be avoided for~$\mathsf{K}$ and~$\mathsf{D}$. In order to prove the former result, we develop a machinery of minimal evidence functions used to effectively build models for justification logics. We observe that the calculus used to construct the minimal functions axiomatizes the reflected fragments of justification logics. We also discuss difficulties that result from an introduction of negative introspection.},
keywords = {self-referentiality},
doi = {10.1007/s00224-009-9209-3},
url = {http://www.iam.unibe.ch/ltgpub/2010/kuz10.pdf},
author = {Roman Kuznets}
}
@article {1341,
title = {Self-Referentiality in Contraction-free Fragments of Modal Logic S4},
year = {2010},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2010/pul10.pdf},
author = {Pulver, Cornelia}
}
@conference {1337,
title = {Two Ways to Common Knowledge},
booktitle = {Proceedings of the 6th~Workshop on Methods for Modalities (M4M{\textendash}6~2009), Copenhagen, Denmark, 12{\textendash}14 November 2009},
series = {Electronic Notes in Theoretical Computer Science},
year = {2010},
pages = {83-98},
publisher = {Elsevier},
organization = {Elsevier},
abstract = {It is not clear what a system for evidence-based common knowledge should look like if common knowledge is treated as a greatest fixed point. This paper is a preliminary step towards such a system. We argue that the standard induction rule is not well suited to axiomatize evidence-based common knowledge. As an alternative, we study two different deductive systems for the logic of common knowledge. The first system makes use of an induction axiom whereas the second one is based on co-inductive proof theory. We show the soundness and completeness for both systems.},
keywords = {proof theory},
doi = {10.1016/j.entcs.2010.04.007},
url = {http://www.iam.unibe.ch/ltgpub/2010/bks10a.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Thomas Bolander and Torben Bra{\"u}ner}
}
@article {1343,
title = {Unfolding finitist arithmetic},
journal = {Review of Symbolic Logic},
volume = {3},
year = {2010},
pages = {665-689},
url = {http://www.iam.unibe.ch/ltgpub/2010/fs10.pdf},
author = {Solomon Feferman and Thomas Strahm}
}
@article {1338,
title = {Verification of Workflow Control-Flow Patterns with the SPIN Model Checker},
year = {2010},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
author = {Stolz, Manuela Claudia}
}
@conference {1339,
title = {Weak theories of operations and types},
booktitle = {Ways of Proof Theory},
year = {2010},
pages = {441-468},
publisher = {Ontos Verlag},
organization = {Ontos Verlag},
url = {http://www.iam.unibe.ch/ltgpub/2010/str10.pdf},
author = {Thomas Strahm},
editor = {Ralf Schindler}
}
@conference {1329,
title = {$Σ^1_1$ choice in a theory of sets and classes},
booktitle = {Ways of Proof Theory},
year = {2010},
pages = {283-314},
publisher = {Ontos Verlag},
organization = {Ontos Verlag},
url = {http://www.iam.unibe.ch/ltgpub/2010/jk10.pdf},
author = {Gerhard J{\"a}ger and Kr{\"a}henb{\"u}hl, J{\"u}rg},
editor = {Ralf Schindler}
}
@conference {1364,
title = {A Note on the Use of Sum in the Logic of Proofs},
booktitle = {Proceedings of the 7th~Panhellenic Logic Symposium},
year = {2009},
pages = {99-103},
publisher = {Patras University Press},
organization = {Patras University Press},
address = {Patras University, Greece},
url = {http://www.iam.unibe.ch/ltgpub/2009/kuz09b.pdf},
author = {Roman Kuznets},
editor = {Costas Drossos and Pavlos Peppas and Constantine Tsinakis}
}
@article {1344,
title = {Aspekte beweisbar totaler Funktionen in applikativen Theorien},
year = {2009},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2009/ebe09.pdf},
author = {Sebastian Eberhard}
}
@article {1345,
title = {Belief Change Functions for Multi-Agent Systems},
year = {2009},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2009/ste09.pdf},
author = {David Steiner}
}
@article {1360,
title = {Common knowledge does not have the Beth property},
journal = {Information Processing Letters},
volume = {109},
year = {2009},
pages = {611-614},
url = {http://www.iam.unibe.ch/ltgpub/2009/stu09.pdf},
author = {Thomas Studer}
}
@conference {1361,
title = {Data Privacy for ALC Knowledge Bases},
booktitle = {Proceedings of Logical Foundations of Computer Science LFCS{\textquoteright}09},
series = {LNCS},
volume = {5407},
year = {2009},
pages = {409-421},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2009/ss09b.pdf},
author = {Phiniki Stouppa and Thomas Studer},
editor = {Sergei Artemov and A. Nerode}
}
@article {1346,
title = {Deciding Data Privacy for ALC Knowledge Bases},
year = {2009},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2009/sto09.pdf},
author = {Phiniki Stouppa}
}
@article {1347,
title = {Deep Sequent Systems for Modal Logic},
journal = {Archive for Mathematical Logic},
volume = {48},
year = {2009},
pages = {551-577},
doi = {10.1007/s00153-009-0137-3},
url = {http://www.iam.unibe.ch/ltgpub/2009/bru09.pdf},
author = {Kai Br{\"u}nnler}
}
@article {1362,
title = {Elementary explicit types and polynomial time operations},
journal = {Mathematical Logic Quarterly},
volume = {55},
year = {2009},
pages = {245-258},
url = {http://www.iam.unibe.ch/ltgpub/2009/ss09a.pdf},
author = {Spescha, Daria and Thomas Strahm}
}
@article {1363,
title = {Full operational set theory with unbounded existential quantification and power set},
journal = {Annals of Pure and Applied Logic},
volume = {160},
year = {2009},
pages = {33-52},
url = {http://www.iam.unibe.ch/ltgpub/2009/jae09a.pdf},
author = {Gerhard J{\"a}ger}
}
@article {1348,
title = {Justifying induction on modal mu-formulae},
year = {2009},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2009/kra09.pdf},
author = {Kr{\"a}henb{\"u}hl, J{\"u}rg}
}
@conference {1349,
title = {Logical Omniscience as a Computational Complexity Problem},
booktitle = {Theoretical Aspects of Rationality and Knowledge, Proceedings of the Twelfth Conference (TARK~2009)},
year = {2009},
pages = {14-23},
publisher = {ACM},
organization = {ACM},
address = {Stanford University, California},
abstract = {The logical omniscience feature assumes that an epistemic agent knows all logical consequences of her assumptions. This paper offers a general theoretical framework that views logical omniscience as a computational complexity problem. We suggest the following approach: we assume that the knowledge of an agent is represented by an epistemic logical system~$E$; we call such an agent \emph{not logically omniscient} if for any valid knowledge assertion~$\mathcal{A}$ of type \emph{$F$~is known}, a proof of~$F$ in~$E$ can be found in polynomial time in the size of~$\mathcal{A}$. We show that agents represented by major modal logics of knowledge and belief are logically omniscient, whereas agents represented by justification logic systems are not logically omniscient with respect to \emph{$t$~is a justification for~$F$}.},
doi = {10.1145/1562814.1562821},
url = {http://www.iam.unibe.ch/ltgpub/2009/ak09.pdf},
author = {Sergei Artemov and Roman Kuznets},
editor = {Aviad Heifetz}
}
@conference {1351,
title = {Modular Sequent Systems for Modal Logic},
booktitle = {Tableaux 2009},
series = {Lecture Notes in Computer Science},
volume = {5607},
year = {2009},
publisher = {Springer-Verlag},
organization = {Springer-Verlag},
doi = {10.1007/978-3-642-02716-1_12},
url = {http://www.iam.unibe.ch/ltgpub/2009/bs09c.pdf},
author = {Kai Br{\"u}nnler and Stra{\ss}burger, Lutz},
editor = {Giese, Martin and Waaler, Arild}
}
@article {1352,
title = {On modal $μ$-calculus and G{\"o}del-L{\"o}b logic},
journal = {Studia Logica},
volume = {91},
year = {2009},
pages = {145-169},
url = {http://www.iam.unibe.ch/ltgpub/2009/af09a.pdf},
author = {Luca Alberucci and Alessandro Facchini}
}
@article {1353,
title = {Ontological Questions about Operational Set Theory},
year = {2009},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2009/zum09.pdf},
author = {Rico Zumbrunnen}
}
@conference {1365,
title = {Operations, sets and classes},
booktitle = {Logic, Methodology and Philosophy of Science - Proceedings of the Thirteenth International Congress},
year = {2009},
publisher = {College Publications},
organization = {College Publications},
url = {http://www.iam.unibe.ch/ltgpub/2009/jae09b.pdf},
author = {Gerhard J{\"a}ger},
editor = {C. Glymour and W. Wei and D. Westerstahl}
}
@article {1354,
title = {Proof-Systems for PLTL: Cycling Sequents and their Use in a Finitization for PLTL},
year = {2009},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2009/tra09.pdf},
author = {Traber, Roger}
}
@article {1355,
title = {Sequent calculi for the modal $μ$-calculus over $\mathsf {S5}$},
journal = {Journal of Logic and Computation},
year = {2009},
note = {Published online on January 22, 2009},
url = {http://www.iam.unibe.ch/ltgpub/2009/alb09.pdf},
author = {Luca Alberucci}
}
@article {1356,
title = {Syntactic cut-elimination for common knowledge},
journal = {Annals of Pure and Applied Logic},
volume = {160},
year = {2009},
pages = {82-95},
doi = {10.1016/j.apal.2009.01.014},
url = {http://www.iam.unibe.ch/ltgpub/2009/bs09b.pdf},
author = {Kai Br{\"u}nnler and Thomas Studer}
}
@conference {1357,
title = {Syntactic cut-elimination for common knowledge},
booktitle = {Proceedings of Methods for Modalities M4M5},
series = {ENTCS},
volume = {231},
year = {2009},
pages = {227-240},
publisher = {Elsevier},
organization = {Elsevier},
doi = {10.1016/j.entcs.2009.02.038},
url = {http://www.iam.unibe.ch/ltgpub/2009/bs09a.pdf},
author = {Kai Br{\"u}nnler and Thomas Studer},
editor = {Areces, C. and Demri, S.}
}
@article {1350,
title = {The modal $μ$-calculus hierarchy over restricted classes of transition systems},
journal = {Journal of Symbolic Logic},
volume = {74},
year = {2009},
pages = {1367-1400},
url = {http://www.iam.unibe.ch/ltgpub/2009/af09b.pdf},
author = {Luca Alberucci and Alessandro Facchini}
}
@conference {1359,
title = {The NP-completeness of reflected fragments of justification logics},
booktitle = {Proceedings of Symposium on Logical Foundations of Computer Science (LFCS{\textquoteright}09)},
series = {Lecture Notes in Computer Science},
volume = {5407},
year = {2009},
pages = {122-136},
abstract = {Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in~NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound.},
doi = {10.1007/978-3-540-92687-0_9},
url = {http://www.iam.unibe.ch/ltgpub/2009/bk09.pdf},
author = {Buss, Samuel R. and Roman Kuznets},
editor = {Sergei Artemov and Nerode, Anil}
}
@article {1358,
title = {Weak Systems of Explicit Mathematics},
year = {2009},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2009/spe09.pdf},
author = {Spescha, Daria}
}
@conference {1375,
title = {An Algorithmic Interpretation of a Deep Inference System},
booktitle = {LPAR 2008},
series = {Lecture Notes in Computer Science},
volume = {5330},
year = {2008},
pages = {482-496},
publisher = {Springer-Verlag},
organization = {Springer-Verlag},
url = {http://www.iam.unibe.ch/ltgpub/2008/bm08.pdf},
author = {Kai Br{\"u}nnler and Richard McKinley},
editor = {Cervesato, I. and Veith, H. and A Voronkov}
}
@article {1366,
title = {Automatic Model Checking of UML models},
year = {2008},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2008/lar08.pdf},
author = {Larrzabal, Ciro}
}
@article {1367,
title = {Canonical completeness of infinitary mu},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
year = {2008},
pages = {270-292},
doi = {10.1016/j.jlap.2008.02.005},
url = {http://www.iam.unibe.ch/ltgpub/2008/jks08.pdf},
author = {Gerhard J{\"a}ger and Mathis Kretz and Thomas Studer}
}
@article {1368,
title = {Cut-free sequent systems for temporal logic},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
year = {2008},
pages = {216-225},
doi = {10.1016/j.jlap.2008.02.004},
url = {http://www.iam.unibe.ch/ltgpub/2008/bl08.pdf},
author = {Kai Br{\"u}nnler and Lange, Martin}
}
@article {1369,
title = {Explicit Mathematics with Positive Existential Stratified Comprehension, Join and Uniform Monotone Inductive Definitions},
year = {2008},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2008/buc08.pdf},
author = {Samuel Bucheli}
}
@book {1370,
title = {G{\"o}del{\textquoteright}s Dialectica Interpretation},
year = {2008},
publisher = {Wiley},
organization = {Wiley},
edition = {Special},
url = {http://onlinelibrary.wiley.com/doi/10.1111/dltc.2008.62.issue-2/issuetoc},
author = {Thomas Strahm}
}
@article {1371,
title = {Introduction},
journal = {Dialectica},
volume = {62},
year = {2008},
pages = {145-147},
doi = {10.1111/j.1746-8361.2008.01143.x},
url = {http://www.iam.unibe.ch/ltgpub/2008/str08b.pdf},
author = {Thomas Strahm}
}
@article {1376,
title = {On contraction and the modal fragment},
journal = {Mathematical Logic Quarterly},
volume = {54},
year = {2008},
pages = {345-349},
url = {http://www.iam.unibe.ch/ltgpub/2008/bps08.pdf},
author = {Kai Br{\"u}nnler and Dieter Probst and Thomas Studer}
}
@article {1372,
title = {On the proof theory of the modal mu-calculus},
journal = {Studia Logica},
volume = {89},
year = {2008},
pages = {343-363},
doi = {10.1007/s11225-008-9133-6},
url = {http://www.iam.unibe.ch/ltgpub/2008/stu08.pdf},
author = {Thomas Studer}
}
@article {1373,
title = {Polytime Functions in Two-Sorted Bounded Arithmetic},
year = {2008},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2008/goe08.pdf},
author = {Remo Goetschi}
}
@article {1377,
title = {Primitive recursive selection functions for existential assertions over abstract algebras},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
year = {2008},
pages = {175-197},
url = {http://www.iam.unibe.ch/ltgpub/2008/sz08.pdf},
author = {Thomas Strahm and Zucker, Jeffery I}
}
@article {1378,
title = {Soft linear set theory},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
year = {2008},
pages = {226-245},
url = {http://www.iam.unibe.ch/ltgpub/2008/mck08.pdf},
author = {Richard McKinley}
}
@article {1374,
title = {The Basic Feasible Functionals in Bounded Arithmetic},
year = {2008},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2008/lin08.pdf},
author = {Liniger, Simone}
}
@article {1380,
title = {A deep inference system for the modal logic $\mathsf S5$},
journal = {Studia Logica},
volume = {85},
year = {2007},
pages = {199-214},
doi = {10.1007/s11225-007-9028-y},
url = {http://www.iam.unibe.ch/ltgpub/2007/sto07.pdf},
author = {Phiniki Stouppa}
}
@conference {1385,
title = {A formal model of data privacy},
booktitle = {Proceedings of Perspectives of System Informatics},
series = {Lecture Notes in Computer Science},
volume = {4378},
year = {2007},
pages = {401-411},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2007/ss07b.pdf},
author = {Phiniki Stouppa and Thomas Studer},
editor = {Irina Virbitskaite and A Voronkov}
}
@article {1382,
title = {A syntactical treatment of simultaneous fixpoints in the modal $μ$-calculus},
year = {2007},
publisher = {Universit{\"a}t Bern},
url = {http://www.iam.unibe.ch/ltgpub/2007/alb07.pdf},
author = {Luca Alberucci}
}
@conference {1384,
title = {Computing with common knowledge},
booktitle = {Proceedings of Artificial Intelligence and Soft Computing},
year = {2007},
pages = {45-50},
publisher = {ACTA Press},
organization = {ACTA Press},
url = {http://www.iam.unibe.ch/ltgpub/2007/weh07a.pdf},
author = {Wehbe, Ricardo},
editor = {Angel P. del Pobil}
}
@article {1379,
title = {Cut-free common knowledge},
journal = {Journal of Applied Logic},
volume = {5},
year = {2007},
pages = {681-689},
doi = {10.1016/j.jal.2006.02.003},
url = {http://www.iam.unibe.ch/ltgpub/2007/jks07.pdf},
author = {Gerhard J{\"a}ger and Mathis Kretz and Thomas Studer}
}
@conference {1386,
title = {Improving semantic query answering},
booktitle = {Proceedings of Database and Expert Systems Applications},
series = {Lecture Notes in Computer Science},
volume = {4653},
year = {2007},
pages = {671-679},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2007/ks07.pdf},
author = {Norbert Kottmann and Thomas Studer},
editor = {Roland Wagner and Norman Revell and G{\"u}nther Pernul}
}
@conference {1387,
title = {Merging rule-based belief databases},
booktitle = {Proceedings of Artificial Intelligence and Applications},
year = {2007},
pages = {585-589},
publisher = {ACTA Press},
organization = {ACTA Press},
url = {http://www.iam.unibe.ch/ltgpub/2007/weh07b.pdf},
author = {Wehbe, Ricardo},
editor = {Vladan Deved{\.z}i{\'c}}
}
@article {1381,
title = {On Feferman{\textquoteright}s operational set theory $\mathsf{OST}$},
journal = {Annals of Pure and Applied Logic},
volume = {150},
year = {2007},
pages = {19-39},
url = {http://www.iam.unibe.ch/ltgpub/2007/jae07.pdf},
author = {Gerhard J{\"a}ger}
}
@conference {1383,
title = {Total public announcements},
booktitle = {Proceedings of Logical Foundations of Computer Science},
series = {Lecture Notes in Computer Science},
volume = {4514},
year = {2007},
pages = {498-511},
publisher = {Springer},
organization = {Springer},
doi = {10.1007/978-3-540-72734-7_35},
url = {http://www.iam.unibe.ch/ltgpub/2007/ss07a.pdf},
author = {David Steiner and Thomas Studer},
editor = {Sergei Artemov and Nerode, Anil}
}
@conference {1396,
title = {A hybrid representation of knowledge and belief},
booktitle = {Proceedings of Formal Approaches to Multi-Agent Systems},
series = {17th biennial European Conference on Artificial Intelligence},
year = {2006},
url = {http://www.iam.unibe.ch/ltgpub/2006/weh06a.pdf},
author = {Wehbe, Ricardo}
}
@conference {1400,
title = {A system for consistency preserving belief change},
booktitle = {Proceedings of Rationality and Knowledge},
series = {18th European Summer School of Logic, Language and Information},
year = {2006},
pages = {133-144},
publisher = {Association for Logic, Language and Information},
organization = {Association for Logic, Language and Information},
url = {http://www.iam.unibe.ch/ltgpub/2006/ste06.pdf},
author = {David Steiner},
editor = {Sergei Artemov and Rohit Parikh}
}
@article {1388,
title = {Cut elimination inside a deep inference system for classical predicate logic},
journal = {Studia Logica},
volume = {82},
year = {2006},
pages = {51-71},
doi = {10.1007/s11225-006-6605-4},
url = {http://www.iam.unibe.ch/ltgpub/2006/bru06a.pdf},
author = {Kai Br{\"u}nnler}
}
@article {1389,
title = {Deduction chains for common knowledge},
journal = {Journal of Applied Logic},
volume = {4},
year = {2006},
pages = {331-357},
doi = {10.1016/j.jal.2005.06.011},
url = {http://www.iam.unibe.ch/ltgpub/2006/ks06.pdf},
author = {Mathis Kretz and Thomas Studer}
}
@conference {1390,
title = {Deep inference and its normal form of derivations},
booktitle = {Proceedings of Computability in Europe},
series = {Lecture Notes in Computer Science},
volume = {3988},
year = {2006},
pages = {65-74},
publisher = {Springer},
organization = {Springer},
doi = {10.1007/11780342_7},
url = {http://www.iam.unibe.ch/ltgpub/2006/bru06b.pdf},
author = {Kai Br{\"u}nnler},
editor = {Arnold Beckmann and Ulrich Berger and Benedikt L{\"o}we and John V. Tucker}
}
@conference {1395,
title = {Deep sequent systems for modal logic},
booktitle = {Proceedings of Advances in Modal Logic},
volume = {6},
year = {2006},
pages = {107-119},
publisher = {College Publications},
organization = {College Publications},
url = {http://www.iam.unibe.ch/ltgpub/2006/bru06c.pdf},
author = {Kai Br{\"u}nnler},
editor = {Guido Governatori and Ian Hodkinson and Yde Venema}
}
@article {1391,
title = {Description Logic Query Answering with Relational Databases},
year = {2006},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2006/kot06.pdf},
author = {Norbert Kottmann}
}
@article {1392,
title = {Explicit Mathematics with Positive Existential Comprehension and Join},
year = {2006},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2006/kra06.pdf},
author = {Kr{\"a}henb{\"u}hl, J{\"u}rg}
}
@article {1393,
title = {Locality for classical logic},
journal = {Notre Dame Journal of Formal Logic},
volume = {47},
year = {2006},
pages = {557-580},
doi = {10.1305/ndjfl/1168352668},
url = {http://www.iam.unibe.ch/ltgpub/2006/bru06d.pdf},
author = {Kai Br{\"u}nnler}
}
@article {1397,
title = {On the proof theory of type two functionals based on primitive recursive operations},
journal = {Mathematical Logic Quarterly},
volume = {52},
year = {2006},
pages = {237-252},
url = {http://www.iam.unibe.ch/ltgpub/2006/ss06.pdf},
author = {David Steiner and Thomas Strahm}
}
@article {1394,
title = {Proof-Theoretic Aspects of Modal Logic with Fixed Points},
year = {2006},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2006/kre06.pdf},
author = {Mathis Kretz}
}
@conference {1399,
title = {Revising non-monotonic rule-based belief databases},
booktitle = {Proceedings of Belief Revision, Belief Merging and Social Choice},
series = {8th Augustus De Morgan Workshop},
year = {2006},
url = {http://www.iam.unibe.ch/ltgpub/2006/weh06b.pdf},
author = {Wehbe, Ricardo}
}
@article {1398,
title = {The proof-theoretic analysis of transfinitely iterated quasi least fixed points},
journal = {The Journal of Symbolic Logic},
volume = {71},
year = {2006},
pages = {721-746},
url = {http://www.iam.unibe.ch/ltgpub/2006/pro06.pdf},
author = {Dieter Probst}
}
@article {1403,
title = {About cut elimination for logics of common knowledge},
journal = {Annals of Pure and Applied Logic},
volume = {133},
year = {2005},
pages = {73-99},
doi = {10.1016/j.apal.2004.10.004},
url = {http://www.iam.unibe.ch/ltgpub/2005/aj05.pdf},
author = {Luca Alberucci and Gerhard J{\"a}ger}
}
@article {1408,
title = {ALOE {\textendash} A Graphical Editor for OWL Ontologies},
year = {2005},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2005/spe05.pdf},
author = {Spescha, Daria}
}
@conference {1409,
title = {Cut-free axiomatizations for stratified modal fixed point logic},
booktitle = {Proceedings of Methods for Modalities 4},
series = {Humboldt-Universit{\"a}t Berlin Informatik-Berichte},
volume = {194},
year = {2005},
pages = {125-143},
publisher = {Humboldt-Universit{\"a}t Berlin},
organization = {Humboldt-Universit{\"a}t Berlin},
url = {http://www.iam.unibe.ch/ltgpub/2005/jks05.pdf},
author = {Gerhard J{\"a}ger and Mathis Kretz and Thomas Studer},
editor = {Holger Schlingloff}
}
@article {1410,
title = {Elementary Arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {133},
year = {2005},
pages = {275-292},
url = {http://www.iam.unibe.ch/ltgpub/2005/ow05.pdf},
author = {Geoffrey E. Ostrin and Stanley S. Wainer}
}
@article {1411,
title = {Explicit mathematics: power types and overloading},
journal = {Annals of Pure and Applied Logic},
volume = {134},
year = {2005},
pages = {284-302},
url = {http://www.iam.unibe.ch/ltgpub/2005/stu05a.pdf},
author = {Thomas Studer}
}
@article {1401,
title = {$\mathcal{PALC}$: Extending $\mathcal{ALC}$ ABoxes with Probabilities},
year = {2005},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2005/due05.pdf},
author = {Michael D{\"u}rig}
}
@article {1402,
title = {$\mathsf{PLTL}$ {\textendash} Vollst{\"a}ndigkeit und Modell-Konstruktion},
year = {2005},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2005/son05.pdf},
author = {Daniel Sonderegger}
}
@conference {1412,
title = {Metapredicative and explicit Mahlo: a proof-theoretic perspective},
booktitle = {Proceedings of Logic Colloquium {\textquoteright}00},
series = {Association of Symbolic Logic Lecture Notes in Logic},
volume = {19},
year = {2005},
pages = {272-293},
publisher = {AK Peters},
organization = {AK Peters},
url = {http://www.iam.unibe.ch/ltgpub/2005/jae05.pdf},
author = {Gerhard J{\"a}ger},
editor = {Rene Cori and Alexander Razborov and Stevo Todorcevic and Carol Wood}
}
@article {1404,
title = {On the Consistency Strength of the Strict $\Pi^1_1$ Reflection Principle},
year = {2005},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2005/sal05.pdf},
author = {Vincenzo Salipante}
}
@article {1413,
title = {On the relationship between fixed points and iteration in admissible set theory without foundation},
journal = {Archive for Mathematical Logic},
volume = {44},
year = {2005},
pages = {561-580},
url = {http://www.iam.unibe.ch/ltgpub/2005/pro05a.pdf},
author = {Dieter Probst}
}
@conference {1414,
title = {On two forms of bureaucracy in derivations},
booktitle = {Proceedings of Structures and Deduction},
year = {2005},
pages = {65-74},
publisher = {Technische Universit{\"a}t Dresden},
organization = {Technische Universit{\"a}t Dresden},
url = {http://www.iam.unibe.ch/ltgpub/2005/bl05.pdf},
author = {Kai Br{\"u}nnler and St{\'e}phane Lengrand},
editor = {Paola Bruscoli and Fran{\c c}ois Lamarche and Charles Stewart}
}
@article {1775,
title = {Papers in Explicit Mathematics},
year = {2005},
url = {http://www.iam.unibe.ch/ltgpub/2016/stu16.pdf},
author = {Thomas Studer}
}
@conference {1415,
title = {Probabilistic ABox reasoning: preliminary results},
booktitle = {Proceedings of Description Logics {\textquoteright}05},
series = {CEUR Workshop Proceedings},
volume = {147},
year = {2005},
pages = {104-111},
publisher = {CEUR-WS.org},
organization = {CEUR-WS.org},
url = {http://www.iam.unibe.ch/ltgpub/2005/ds05.pdf},
author = {Michael D{\"u}rig and Thomas Studer},
editor = {Ian Horrocks and Ulrike Sattler and Frank Wolter}
}
@conference {1416,
title = {Provable data privacy},
booktitle = {Proceedings of 16th International Conference on Database and Expert Systems Applications},
series = {Lecture Notes in Computer Science},
volume = {3588},
year = {2005},
pages = {324-332},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2005/ss05.pdf},
author = {Kilian Stoffel and Thomas Studer},
editor = {Kim Viborg Andersen and John K. Debenham and Roland Wagner}
}
@article {1405,
title = {Pseudo-Hierarchies in Admissible Set Theory without Foundation and Explicit Mathematics},
year = {2005},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2005/pro05b.pdf},
author = {Dieter Probst}
}
@article {1417,
title = {Reflections on reflections in explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {136},
year = {2005},
pages = {116-133},
url = {http://www.iam.unibe.ch/ltgpub/2005/js05.pdf},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@conference {1406,
title = {Relational representation of $\mathcal{ALN}$ knowledge bases},
booktitle = {Proceedings of Multi {\textquoteright}05},
year = {2005},
pages = {271-278},
publisher = {International Association for Development of the Information Society},
organization = {International Association for Development of the Information Society},
url = {http://www.iam.unibe.ch/ltgpub/2005/stu05b.pdf},
author = {Thomas Studer},
editor = {Pedro Isa{\'\i}as and Miguel B. Nunes and Antonio Palma dos Reis}
}
@article {1407,
title = {Wellordering Two Sorts: A Slow-Growing Proof Theory for Variable Separation},
year = {2005},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2005/wir05.pdf},
author = {Marc Wirz}
}
@article {1422,
title = {A proof-theoretic characterization of the basic feasible functionals},
journal = {Theoretical Computer Science},
volume = {329},
year = {2004},
pages = {159-176},
url = {http://www.iam.unibe.ch/ltgpub/2004/str04.pdf},
author = {Thomas Strahm}
}
@article {1421,
title = {An intensional fixed point theory over first order arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {128},
year = {2004},
pages = {197-213},
url = {http://www.iam.unibe.ch/ltgpub/2004/jae04.pdf},
author = {Gerhard J{\"a}ger}
}
@conference {1418,
title = {Iterating $Σ$ operations in admissible set theory without foundation: a further aspect of metapredicative Mahlo},
booktitle = {One Hundred Years of Russell{\textquoteright}s Paradox. Papers from the 2001 Munich Russell Conference},
year = {2004},
pages = {119-134},
publisher = {de Gruyter},
organization = {de Gruyter},
url = {http://www.iam.unibe.ch/ltgpub/2004/jp04a.pdf},
author = {Gerhard J{\"a}ger and Dieter Probst},
editor = {Godehart Link}
}
@article {1419,
title = {On modal $μ$-calculus and non-well-founded set theory},
journal = {Journal of Philosophical Logic},
volume = {33},
year = {2004},
pages = {343-360},
url = {http://www.iam.unibe.ch/ltgpub/2004/as04.pdf},
author = {Luca Alberucci and Vincenzo Salipante}
}
@article {1423,
title = {Variation on a theme of Sch{\"u}tte},
journal = {Mathematical Logic Quarterly},
volume = {50},
year = {2004},
pages = {258-264},
url = {http://www.iam.unibe.ch/ltgpub/2004/jp04b.pdf},
author = {Gerhard J{\"a}ger and Dieter Probst}
}
@article {1420,
title = {Weak K{\"o}nig{\textquoteright}s Lemma and Extensional Equality},
year = {2004},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2004/bur04.pdf},
author = {Theo Burri}
}
@article {1426,
title = {Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe},
journal = {Annals of Pure and Applied Logic},
volume = {120},
year = {2003},
pages = {165-196},
url = {http://www.iam.unibe.ch/ltgpub/2003/tup03.ps},
author = {Sergei Tupailo}
}
@article {1424,
title = {The proof-theoretic analysis of $Σ^1_1$ transfinite dependent choice},
journal = {Annals of Pure and Applied Logic},
volume = {122},
year = {2003},
pages = {195-234},
url = {http://www.iam.unibe.ch/ltgpub/2003/rue03a.pdf},
author = {Christian R{\"u}ede}
}
@article {1427,
title = {Theories with self-application and computational complexity},
journal = {Information and Computation},
volume = {185},
year = {2003},
pages = {263-297},
url = {http://www.iam.unibe.ch/ltgpub/2003/str03.pdf},
author = {Thomas Strahm}
}
@article {1425,
title = {Two Interpretations of $\mathsf{WKL}_0$ in Subsystems of $\mathsf{PA}$},
year = {2003},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2003/sch03.pdf},
author = {Thomas Schweizer}
}
@article {1428,
title = {Universes in metapredicative analysis},
journal = {Archive for Mathematical Logic},
volume = {42},
year = {2003},
pages = {129-151},
url = {http://www.iam.unibe.ch/ltgpub/2003/rue03b.pdf},
author = {Christian R{\"u}ede}
}
@article {1429,
title = {Extending the system $\mathsf{T}_0$ of explicit mathematics: the limit and Mahlo axioms},
journal = {Annals of Pure and Applied Logic},
volume = {114},
year = {2002},
pages = {79-101},
url = {http://www.iam.unibe.ch/ltgpub/2002/js02b.pdf},
author = {Gerhard J{\"a}ger and Thomas Studer}
}
@article {1430,
title = {Information Flow {\textendash} Logics for the (R)age of Information},
year = {2002},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2002/kel02.pdf},
author = {Philipp Keller}
}
@article {1437,
title = {Intuitionistic fixed point theories for strictly positive operators},
journal = {Mathematical Logic Quarterly},
volume = {48},
year = {2002},
pages = {195-202},
url = {http://www.iam.unibe.ch/ltgpub/2002/rs02.pdf},
author = {Christian R{\"u}ede and Thomas Strahm}
}
@article {1432,
title = {On the Treatment of Predicative Polymorphism in Theories of Explicit Mathematics},
year = {2002},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2002/kre02.pdf},
author = {Mathis Kretz}
}
@conference {1433,
title = {Proof theoretic complexity},
booktitle = {Proof and System Reliability},
series = {NATO Science Series},
volume = {62},
year = {2002},
pages = {369-398},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2002/ow02.pdf},
author = {Geoffrey E. Ostrin and Stanley S. Wainer},
editor = {Helmut Schwichtenberg and Ralf Steinbr{\"u}ggen}
}
@conference {1435,
title = {Strictness of the modal $μ$-calculus hierarchy},
booktitle = {Automata, Logics and infinite Games: A Guide to Current Research},
series = {Lecture Notes in Computer Science},
volume = {2500},
year = {2002},
pages = {185-201},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2002/alb02b.ps},
author = {Luca Alberucci},
editor = {Erich Gr{\"a}del and Wolfgang Thomas and Thomas Wilke}
}
@article {1431,
title = {The Modal $μ$-Calculus and the Logic of Common Knowledge},
year = {2002},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2002/alb02a.pdf},
author = {Luca Alberucci}
}
@conference {1434,
title = {The proof-theoretic analysis of the Suslin operator in applicative theories},
booktitle = {Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman},
year = {2002},
pages = {270-292},
publisher = {AK Peters},
organization = {AK Peters},
url = {http://www.iam.unibe.ch/ltgpub/2002/js02a.pdf},
author = {Gerhard J{\"a}ger and Thomas Strahm},
editor = {Wilfried Sieg and Richard Sommer and Carolyn Talcott}
}
@article {1436,
title = {Transfinite dependent choice and $\omega$-model reflection},
journal = {The Journal of Symbolic Logic},
volume = {67},
year = {2002},
pages = {1153-1168},
url = {http://www.iam.unibe.ch/ltgpub/2002/rue02.pdf},
author = {Christian R{\"u}ede}
}
@article {1438,
title = {Wellordering proofs for metapredicative Mahlo},
journal = {The Journal of Symbolic Logic},
volume = {67},
year = {2002},
pages = {260-278},
url = {http://www.iam.unibe.ch/ltgpub/2002/str02.pdf},
author = {Thomas Strahm}
}
@article {1443,
title = {A semantics for $\lambda^{\{\}}_{\mathsf str}$: a calculus with overloading and late-binding},
journal = {Journal of Logic and Computation},
volume = {11},
year = {2001},
pages = {527-544},
url = {http://www.iam.unibe.ch/ltgpub/2001/stu01a.pdf},
author = {Thomas Studer}
}
@conference {1445,
title = {Constructive foundations for Featherweight Java},
booktitle = {Proceedings of the International Seminar on Proof Theory in Computer Science},
series = {Lecture Notes in Computer Science},
volume = {2183},
year = {2001},
pages = {202-238},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2001/stu01b.pdf},
author = {Thomas Studer},
editor = {Reinhard Kahle and Peter Schroeder-Heister and Robert F. St{\"a}rk}
}
@article {1446,
title = {First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo},
journal = {The Journal of Symbolic Logic},
volume = {66},
year = {2001},
pages = {1073-1089},
url = {http://www.iam.unibe.ch/ltgpub/2001/jae01.pdf},
author = {Gerhard J{\"a}ger}
}
@article {1447,
title = {Formalizing non-termination of recursive programs},
journal = {Journal of Logic and Algebraic Programming},
volume = {49},
year = {2001},
pages = {1-14},
url = {http://www.iam.unibe.ch/ltgpub/2001/ks01.pdf},
author = {Reinhard Kahle and Thomas Studer}
}
@article {1448,
title = {How to normalize the Jay},
journal = {Theoretical Computer Science},
volume = {254},
year = {2001},
pages = {677-681},
url = {http://www.iam.unibe.ch/ltgpub/2001/ps01.pdf},
author = {Dieter Probst and Thomas Studer}
}
@article {1440,
title = {Object-Oriented Programming in Explicit Mathematics: Towards the Mathematics of Objects},
year = {2001},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2001/stu01c.pdf},
author = {Thomas Studer}
}
@article {1441,
title = {Proof-theoretic contributions to explicit mathematics},
year = {2001},
publisher = {Universit{\"a}t Bern},
type = {Habilitationsschrift},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2001/str01.pdf},
author = {Thomas Strahm}
}
@article {1442,
title = {Proof-Theoretic Strength of $\mathsf{PRON}$ with Various Extensions},
year = {2001},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2001/ste01.pdf},
author = {David Steiner}
}
@article {1449,
title = {Realization of analysis into explicit mathematics},
journal = {The Journal of Symbolic Logic},
volume = {66},
year = {2001},
pages = {1848-1864},
url = {http://www.iam.unibe.ch/ltgpub/2001/tup01.pdf},
author = {Sergei Tupailo}
}
@article {1439,
title = {The MacLWB and the Logic of Likelihood},
year = {2001},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2001/bal01.pdf},
author = {Peter Balsiger}
}
@article {1444,
title = {Theories of Ordinal Strength $\varphi 2 0$ and $\varphi 2 \varepsilon_0$},
year = {2001},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2001/hei01.pdf},
author = {Marc Heissenb{\"u}ttel}
}
@article {1450,
title = {Universes in explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {109},
year = {2001},
pages = {141-162},
url = {http://www.iam.unibe.ch/ltgpub/2001/jks01.pdf},
author = {Gerhard J{\"a}ger and Reinhard Kahle and Thomas Studer}
}
@article {1451,
title = {Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory},
journal = {The Journal of Symbolic Logic},
volume = {66},
year = {2001},
pages = {935-958},
url = {http://www.iam.unibe.ch/ltgpub/2001/js01.pdf},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1458,
title = {A benchmark method for the propositional modal logics K, KT, S4},
journal = {Journal of Automated Reasoning},
volume = {24},
year = {2000},
pages = {297-317},
url = {http://www.iam.unibe.ch/ltgpub/2000/bhs00.pdf},
author = {Peter Balsiger and Alain Heuerding and Stefan Schwendimann}
}
@conference {1454,
title = {A theory of explicit mathematics equivalent to ${ \mathsf{ID} }_1$},
booktitle = {Proceedings of Computer Science Logic},
series = {Lecture Notes in Computer Science},
volume = {1862},
year = {2000},
pages = {356-370},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/2000/ks00.pdf},
author = {Reinhard Kahle and Thomas Studer},
editor = {Peter Clote and Helmut Schwichtenberg}
}
@conference {1457,
title = {Autonomous fixed point progressions and fixed point transfinite recursion},
booktitle = {Proceedings of Logic Colloquium {\textquoteright}98},
series = {Association of Symbolic Logic Lecture Notes in Logic},
volume = {13},
year = {2000},
pages = {449-464},
publisher = {AK Peters},
organization = {AK Peters},
url = {http://www.iam.unibe.ch/ltgpub/2000/str00a.pdf},
author = {Thomas Strahm},
editor = {Samuel S. Buss and Petr Hajek and Pavel Pudlak}
}
@article {1455,
title = {Einige Aspekte der Modallogik $\mathsf{S5}_n$ mit Allgemeinwissen},
year = {2000},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2000/kre00.pdf},
author = {Michel Krebs}
}
@conference {1459,
title = {Finitary reductions for local predicativity, I: recursively regular ordinals},
booktitle = {Proceedings of Logic Colloquium {\textquoteright}98},
series = {Association of Symbolic Logic Lecture Notes in Logic},
volume = {13},
year = {2000},
pages = {465-499},
publisher = {AK Peters},
organization = {AK Peters},
author = {Sergei Tupailo},
editor = {Samuel S. Buss and Petr Hajek and Pavel Pudlak}
}
@article {1460,
title = {Fixed point theories and dependent choice},
journal = {Archive for Mathematical Logic},
volume = {39},
year = {2000},
pages = {493-508},
url = {http://www.iam.unibe.ch/ltgpub/2000/js00.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1452,
title = {Metapredicative Subsystems of Analysis},
year = {2000},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/2000/rue00.pdf},
author = {Christian R{\"u}ede}
}
@article {1456,
title = {N-strictness in applicative theories},
journal = {Archive for Mathematical Logic},
volume = {39},
year = {2000},
pages = {125-144},
doi = {10.1007/s001530050007},
url = {http://dx.doi.org/10.1007/s001530050007},
author = {Reinhard Kahle}
}
@article {1453,
title = {The non-constructive $μ$-operator, fixed point theories with ordinals, and the bar rule},
journal = {Annals of Pure and Applied Logic},
volume = {104},
year = {2000},
pages = {305-324},
url = {http://www.iam.unibe.ch/ltgpub/2000/str00b.ps},
author = {Thomas Strahm}
}
@article {1461,
title = {The unfolding of non-finitist arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {104},
year = {2000},
pages = {75-96},
url = {http://www.iam.unibe.ch/ltgpub/2000/fs00.ps},
author = {Solomon Feferman and Thomas Strahm}
}
@article {1470,
title = {A semantics for $\lambda^{ \{ \} }_{ \mathsf {str }}$: a calculus with overloading and late-binding},
year = {1999},
publisher = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1999/stu99.ps},
author = {Thomas Studer}
}
@article {1462,
title = {Bar induction and $\omega$ model reflection},
journal = {Annals of Pure and Applied Logic},
volume = {97},
year = {1999},
pages = {221-230},
url = {http://www.iam.unibe.ch/ltgpub/1999/js99.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1463,
title = {Characterizing the Grzegorczyk hierarchy by safe recursion},
year = {1999},
publisher = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1999/wir99a.pdf},
author = {Marc Wirz}
}
@article {1471,
title = {Charakterisierungen kleiner Komplexit{\"a}tsklassen mittels geschichteter N-Pr{\"a}dikate},
year = {1999},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1999/wir99b.pdf},
author = {Marc Wirz}
}
@article {1464,
title = {Dependent Choice in Explicit Mathematics},
year = {1999},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1999/pro99.pdf},
author = {Dieter Probst}
}
@conference {1465,
title = {Epsilon-substitution method for the ramified language and $Δ^1_1$-comprehension rule},
booktitle = {Logic and Foundation of Mathematics},
year = {1999},
pages = {107-130},
publisher = {Kluwer},
organization = {Kluwer},
author = {Grigori Mints and Sergei Tupailo},
editor = {Andrea Cantini and Ettore Casari and Pierluigi Minari}
}
@article {1466,
title = {Extension of the Modal System KT4},
year = {1999},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
author = {Irene Bucher}
}
@conference {1467,
title = {First steps into metapredicativity in explicit mathematics},
booktitle = {Sets and Proofs},
series = {London Mathematical Society Lecture Notes},
volume = {258},
year = {1999},
pages = {383-402},
publisher = {Cambridge University Press},
organization = {Cambridge University Press},
url = {http://www.iam.unibe.ch/ltgpub/1999/str99.pdf},
author = {Thomas Strahm},
editor = {S. Barry Cooper and John K. Truss}
}
@article {1472,
title = {Konstruktion von Gegenmodellen intuitionistisch unbeweisbarer Sequenzen},
year = {1999},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
author = {Jimmy Brignioni}
}
@article {1468,
title = {Logics Workbench f{\"u}r Window System},
year = {1999},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
author = {Afshin D. Boroumand}
}
@conference {1469,
title = {On applicative theories},
booktitle = {Logic and Foundations of Mathematics},
year = {1999},
pages = {83-92},
publisher = {Kluwer},
organization = {Kluwer},
url = {http://www.iam.unibe.ch/ltgpub/1999/jks99.ps},
author = {Gerhard J{\"a}ger and Reinhard Kahle and Thomas Strahm},
editor = {Andrea Cantini and Ettore Casari and Pierluigi Minari}
}
@article {1473,
title = {The proof-theoretic analysis of transfinitely iterated fixed point theories},
journal = {The Journal of Symbolic Logic},
volume = {64},
year = {1999},
pages = {53-67},
url = {http://www.iam.unibe.ch/ltgpub/1999/jkss99.ps},
author = {Gerhard J{\"a}ger and Reinhard Kahle and Anton Setzer and Thomas Strahm}
}
@conference {1481,
title = {A new one-pass tableau calculus for $\mathsf{PLTL}$},
booktitle = {Proceedings of Tableaux {\textquoteright}98},
series = {Lecture Notes in Computer Science},
volume = {1397},
year = {1998},
pages = {277-292},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/1998/sch98a.ps},
author = {Stefan Schwendimann},
editor = {Harrie C. M. de Swart}
}
@conference {1476,
title = {A proof-theoretic framework for logic programming},
booktitle = {Handbook of Proof Theory},
year = {1998},
pages = {639-682},
publisher = {North-Holland},
organization = {North-Holland},
doi = {10.1016/S0049-237X(98)80024-4},
url = {http://dx.doi.org/10.1016/S0049-237X(98)80024-4},
author = {Gerhard J{\"a}ger and Robert F. St{\"a}rk},
editor = {Samuel S. Buss}
}
@article {1475,
title = {Aspects of Computational Logic},
year = {1998},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1998/sch98b.ps},
author = {Stefan Schwendimann}
}
@conference {1480,
title = {Comparison of Theorem Provers for Modal Logics {\textendash} Introduction and Summary},
booktitle = {Proceedings of Tableaux {\textquoteright}98},
series = {Lecture Notes in Computer Science},
volume = {1397},
year = {1998},
pages = {25-26},
publisher = {Springer},
organization = {Springer},
author = {Peter Balsiger and Alain Heuerding},
editor = {Harrie C. M. de Swart}
}
@article {1479,
title = {Frege structures for partial applicative theories},
journal = {Journal of Logic and Computation},
volume = {8},
year = {1998},
pages = {683-700},
doi = {10.1093/logcom/9.5.683},
url = {http://dx.doi.org/10.1093/logcom/9.5.683},
author = {Reinhard Kahle}
}
@conference {1482,
title = {Logics Workbench 1.0},
booktitle = {Proceedings of Tableaux {\textquoteright}98},
series = {Lecture Notes in Computer Science},
volume = {1397},
year = {1998},
pages = {35-37},
publisher = {Springer},
organization = {Springer},
author = {Peter Balsiger and Alain Heuerding},
editor = {Harrie C. M. de Swart}
}
@conference {1477,
title = {Relation Algebra and Modal Logics},
booktitle = {Relational Methods in Computer Science},
series = {Advances in Computer Science},
year = {1998},
pages = {20-89},
publisher = {Springer},
organization = {Springer},
author = {Holger Schlingloff and Wolfgang Heinle},
editor = {Chris Brink and Wolfram Kahl and Gunther Schmidt}
}
@article {1478,
title = {Sequent Calculi for Proof Search in some Modal Logics},
year = {1998},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1998/heu98.pdf},
author = {Alain Heuerding}
}
@article {1474,
title = {The $μ$ quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals},
journal = {Archive for Mathematical Logic},
volume = {37},
year = {1998},
pages = {391-413},
url = {http://www.iam.unibe.ch/ltgpub/1998/ms98.ps},
author = {Markus Marzetta and Thomas Strahm}
}
@article {1483,
title = {Applikative Theorien und Frege-Strukturen},
year = {1997},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1997/kah97a.ps},
author = {Reinhard Kahle}
}
@article {1484,
title = {Explicit Mathematics: W-type, Models},
year = {1997},
publisher = {Universit{\"a}t Bern},
type = {masters},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1997/stu97.ps},
author = {Thomas Studer}
}
@conference {1490,
title = {Hybrid spectral transform diagrams},
booktitle = {Proceedings of the International Conference on Information and Communications Security},
series = {Lecture Notes in Computer Science},
volume = {1334},
year = {1997},
pages = {251-255},
publisher = {Springer},
organization = {Springer},
author = {E. Clarke and Masayuki Fujita and Wolfgang Heinle},
editor = {Yongfei Han and Tatsuaki Okamoto and Sihan Qing}
}
@article {1485,
title = {Hybrid spectral transform diagrams},
year = {1997},
publisher = {Carnegie Mellon University},
address = {Department of Computer Science},
author = {E. Clarke and Masayuki Fujita and Wolfgang Heinle}
}
@article {1486,
title = {Modal rule correspondences},
year = {1997},
publisher = {Universit{\"a}t Bern},
type = {Dagstuhl Seminar report},
author = {Wolfgang Heinle and Holger Schlingloff}
}
@conference {1487,
title = {Model checking},
booktitle = {Handbook of Automated Reasoning},
year = {1997},
pages = {1635-1790},
publisher = {Elsevier Science},
organization = {Elsevier Science},
author = {E. Clarke and Wolfgang Heinle and Holger Schlingloff},
editor = {Alan Robinson and A Voronkov}
}
@article {1491,
title = {Polynomial time operations in explicit mathematics},
journal = {The Journal of Symbolic Logic},
volume = {62},
year = {1997},
pages = {575-594},
url = {http://www.iam.unibe.ch/ltgpub/1997/str97.ps},
author = {Thomas Strahm}
}
@article {1492,
title = {Power types in explicit mathematics?},
journal = {The Journal of Symbolic Logic},
volume = {62},
year = {1997},
pages = {1142-1146},
url = {http://www.jstor.org/stable/2275630},
author = {Gerhard J{\"a}ger}
}
@article {1493,
title = {Relations between propositional normal modal logics: an overview},
journal = {Journal of Logic and Computation},
volume = {7},
year = {1997},
pages = {649-658},
url = {http://www.iam.unibe.ch/ltgpub/1997/ghh97.ps},
author = {Rajeev Gor{\'e} and Wolfgang Heinle and Alain Heuerding}
}
@conference {1488,
title = {Some proof theory of first order logic programming},
booktitle = {Logic of Computation},
series = {NATO Science Series},
volume = {157},
year = {1997},
pages = {201-228},
publisher = {Springer},
organization = {Springer},
author = {Gerhard J{\"a}ger},
editor = {Helmut Schwichtenberg}
}
@article {1489,
title = {Uniform limit in explicit mathematics with universes},
year = {1997},
publisher = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1997/kah97b.ps},
author = {Reinhard Kahle}
}
@article {1494,
title = {A benchmark method for the propositional modal logics K, KT, S4},
year = {1996},
publisher = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1996/hs96b.ps},
author = {Alain Heuerding and Stefan Schwendimann}
}
@article {1502,
title = {A logics workbench},
journal = {The European Journal on Artificial Intelligence},
volume = {9},
year = {1996},
pages = {53-58},
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan Schwendimann and Michael Seyfried}
}
@conference {1501,
title = {Efficient loop-check for backward proof search in some non-classical propositional logics},
booktitle = {Proceedings of Tableaux {\textquoteright}96},
series = {Lecture Notes in Computer Science},
volume = {1071},
year = {1996},
pages = {210-225},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/1996/hsz96.ps},
author = {Alain Heuerding and Michael Seyfried and Heinrich Zimmermann},
editor = {Pierangelo Miglioli and Ugo Moscato and Daniele Mundici and Mario Ornaghi}
}
@article {1500,
title = {Frege structures for partial applicative theories},
year = {1996},
publisher = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
author = {Reinhard Kahle}
}
@article {1506,
title = {LWBtheory: information about some propositional logics via the WWW},
journal = {Journal of the Interest Group in Pure and Applied Logic},
volume = {4},
year = {1996},
pages = {196-174},
url = {http://www.iam.unibe.ch/ltgpub/1996/heu96.ps},
author = {Alain Heuerding}
}
@conference {1504,
title = {On the modal logic K plus theories},
booktitle = {Proceedings of Computer Science Logic {\textquoteright}95},
series = {Lecture Notes in Computer Science},
volume = {1092},
year = {1996},
pages = {308-319},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/1996/hs96a.ps},
author = {Alain Heuerding and Stefan Schwendimann},
editor = {Hans Kleine B{\"u}ning}
}
@article {1495,
title = {On the Proof Theory of Applicative Theories},
year = {1996},
publisher = {Universit{\"a}t Bern},
type = {phd},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1996/str96a.ps},
author = {Thomas Strahm}
}
@article {1505,
title = {Partial applicative theories and explicit substitutions},
journal = {Journal of Logic and Computation},
volume = {6},
year = {1996},
pages = {55-77},
url = {http://www.iam.unibe.ch/ltgpub/1996/str96b.ps},
author = {Thomas Strahm}
}
@article {1496,
title = {Some theories with positive induction of ordinal strength $\varphi \omega 0$},
journal = {The Journal of Symbolic Logic},
volume = {61},
year = {1996},
pages = {818-842},
url = {http://www.iam.unibe.ch/ltgpub/1996/js96.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1497,
title = {Systems of explicit mathematics with non-constructive $μ$-operator and join},
journal = {Annals of Pure and Applied Logic},
volume = {82},
year = {1996},
pages = {193-219},
url = {http://www.iam.unibe.ch/ltgpub/1996/gs96.ps},
author = {Thomas Glass and Thomas Strahm}
}
@article {1498,
title = {Systems of explicit mathematics with non-constructive $μ$-operator. Part II},
journal = {Annals of Pure and Applied Logic},
volume = {79},
year = {1996},
pages = {37-52},
doi = {10.1016/0168-0072(95)00028-3},
url = {http://dx.doi.org/10.1016/0168-0072(95)00028-3},
author = {Solomon Feferman and Gerhard J{\"a}ger}
}
@article {1503,
title = {The logics workbench LWB: a snapshot},
journal = {Euromath Bulletin},
volume = {2},
year = {1996},
pages = {177-186},
url = {http://www.iam.unibe.ch/ltgpub/1996/hjss96b.ps},
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan Schwendimann and Michael Seyfried}
}
@article {1499,
title = {Universes over Frege Structures},
year = {1996},
publisher = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1996/kah96a.ps},
author = {Reinhard Kahle}
}
@conference {1508,
title = {A deductive approach to logic programming},
booktitle = {Proof and Computation},
series = {NATO ASI Series F},
volume = {139},
year = {1995},
pages = {231-270},
publisher = {Springer},
organization = {Springer},
author = {Gerhard J{\"a}ger},
editor = {Helmut Schwichtenberg}
}
@conference {1513,
title = {LWB - a logics workbench, extended abstract},
booktitle = {Proceedings of KI-95 Activities: Workshop, Posters, Demos},
year = {1995},
pages = {73-74},
publisher = {Gesellschaft f{\"u}r Informatik},
organization = {Gesellschaft f{\"u}r Informatik},
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan Schwendimann and Michael Seyfried},
editor = {L. Dreschler-Fischer and S. Pribbenow}
}
@article {1507,
title = {Natural numbers and forms of weak induction in applicative theories},
year = {1995},
publisher = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://www.iam.unibe.ch/ltgpub/1995/kah95.ps},
author = {Reinhard Kahle}
}
@conference {1509,
title = {Propositional logics on the computer},
booktitle = {Proceedings of Theorem Proving with Analytic Tableaux and Related Methods},
series = {Lecture Notes in Computer Science},
volume = {918},
year = {1995},
pages = {310-323},
publisher = {Springer},
organization = {Springer},
url = {http://www.iam.unibe.ch/ltgpub/1995/hjss95a.ps},
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan Schwendimann and Michael Seyfried},
editor = {Peter Baumgartner and Reiner H{\"a}hnle and Joachim Posegga}
}
@conference {1510,
title = {Relational semantics for modal logics},
booktitle = {Proceedings of Verification in New Orientations},
year = {1995},
pages = {104-131},
publisher = {University of Maribor},
organization = {University of Maribor},
url = {http://www.iam.unibe.ch/ltgpub/1995/hs95.ps},
author = {Wolfgang Heinle and Bernd-Holger Schlingloff},
editor = {Robert Rodosek}
}
@article {1511,
title = {Second order theories with ordinals and elementary comprehension},
journal = {Archive for Mathematical Logic},
volume = {34},
year = {1995},
pages = {345-375},
url = {http://www.iam.unibe.ch/ltgpub/1995/js95a.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1512,
title = {Totality in applicative theories},
journal = {Annals of Pure and Applied Logic},
volume = {74},
year = {1995},
pages = {105-120},
url = {http://www.iam.unibe.ch/ltgpub/1995/js95b.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1514,
title = {About some symmetries of negation},
journal = {The Journal of Symbolic Logic},
volume = {59},
year = {1994},
pages = {473-485},
url = {http://www.jstor.org/stable/2275401},
author = {Brigitte H{\"o}sli and Gerhard J{\"a}ger}
}
@conference {1516,
title = {Executable models for analysis and implementation of complex systems},
booktitle = {Proceedings of Information Conference of Swiss Priority Programme Informatics Research 1992{\textendash}1996, Module 1: Secure Distributed Systems},
year = {1994},
author = {B. B{\"u}tler and R. Esser and Gerhard J{\"a}ger and Urs-Martin K{\"u}nzi and Heinz Lienhard and R. Mattmann}
}
@article {1515,
title = {The basic logic of proofs},
year = {1994},
publisher = {University of Bern},
type = {phd},
abstract = {Propositional Provability Logic was axiomatized by R. M. Solovay in 1976. This modal logic describes the behavior of the arithmetical operator {\textquoteleft}{\textquoteleft}\$A\$ is provable{\textquoteright}{\textquoteright}. The aim of these investigations is to provide propositional axiomatizations of the predicates {\textquoteleft}{\textquoteleft}\$p\$ is a proof of \$A\${\textquoteright}{\textquoteright}, {\textquoteleft}{\textquoteleft}\$p\$ is a proof which contains \$A\${\textquoteright}{\textquoteright} and {\textquoteleft}{\textquoteleft}\$p\$ is a program which computes \$A\${\textquoteright}{\textquoteright} using the same semantics. The presented systems, called the Basic Logic of Proofs, are first proved to be sound and complete with respect to arithmetical interpretations. Decidability is a consequence of a semantical cut elimination theorem. Moreover, appropriate syntactical models for the Basic Logic of Proofs are defined, which are closely related to canonical models. Finally, some general principles of the Basic Logic of Proofs, mainly concerning fixed points, are investigated.},
url = {http://www.strassen.us/thesis.pdf},
author = {Tyko Strassen}
}
@article {1517,
title = {Fixed points in Peano arithmetic with ordinals},
journal = {Annals of Pure and Applied Logic},
volume = {60},
year = {1993},
pages = {119-132},
doi = {10.1016/0168-0072(93)90039-G},
url = {http://dx.doi.org/10.1016/0168-0072(93)90039-G},
author = {Gerhard J{\"a}ger}
}
@article {1521,
title = {Functionality in the Basic Logic of Proofs},
year = {1993},
publisher = {Institut f{\"u}r Informatik und angewandte Mathematik},
abstract = {This report describes the elimination of the injectivity restriction for functional arithmetical interpretations as used in the systems~$\mathcal{PF}$ and~$\mathcal{PFM}$ in the Basic Logic of Proofs. An appropriate axiom system~$\mathcal{PU}$ in a language with operators {\textquoteleft}{\textquoteleft}$x$~is a proof of~$y${\textquoteright}{\textquoteright} is defined and proved to be sound and complete with respect to all arithmetical interpretations based on functional proof predicates. Unification plays a major role in the formulation of the new axioms.},
url = {http://www.iam.unibe.ch/publikationen/techreports/1993/iam-93-004},
author = {Sergei Artemov and Tyko Strassen}
}
@conference {1523,
title = {Some proof-theoretic aspects of logic programming},
booktitle = {Logic and Algebra of Specification},
series = {Computer and Systems Sciences},
volume = {94},
year = {1993},
pages = {113-142},
publisher = {Springer},
organization = {Springer},
author = {Gerhard J{\"a}ger},
editor = {Friedrich Ludwig Bauer and Wilfried Brauer and Helmut Schwichtenberg}
}
@article {1518,
title = {Systems of explicit mathematics with non-constructive $μ$-operator. Part I},
journal = {Annals of Pure and Applied Logic},
volume = {65},
year = {1993},
pages = {243-263},
url = {http://www.iam.unibe.ch/ltgpub/1993/fj93.pdf},
author = {Solomon Feferman and Gerhard J{\"a}ger}
}
@conference {1519,
title = {The Basic Logic of Proofs},
booktitle = {Computer Science Logic, 6th Workshop, CSL{\textquoteright}92, San Miniato, Italy, September 28{\textendash}October 2, 1992, Selected Papers},
series = {Lecture Notes in Computer Science},
volume = {702},
year = {1993},
pages = {14-28},
publisher = {Springer},
organization = {Springer},
abstract = {Propositional Provability Logic was axiomatized in~[Sol76]. This logic describes the behaviour of the arithmetical operator {\textquoteleft}{\textquoteleft}$y$~is provable{\textquoteright}{\textquoteright}. The aim of the current paper is to provide propositional axiomatizations of the predicate {\textquoteleft}{\textquoteleft}$x$~is a proof of~$y${\textquoteright}{\textquoteright} by means of modal logic, with the intention of meeting some of the needs of computer science.},
doi = {10.1007/3-540-56992-8_3},
author = {Sergei Artemov and Tyko Strassen},
editor = {E. B{\"o}rger and Gerhard J{\"a}ger and Kleine B{\"u}ning, H. and S. Martini and M. M. Richter}
}
@article {1520,
title = {The defining power of stratified and hierarchical logic programs},
journal = {Journal of Logic Programming},
volume = {15},
year = {1993},
pages = {55-77},
url = {http://www.iam.unibe.ch/ltgpub/1993/js93.pdf},
author = {Gerhard J{\"a}ger and Robert F. St{\"a}rk}
}
@conference {1522,
title = {The Logic of the G{\"o}del Proof Predicate},
booktitle = {Computational Logic and Proof Theory, Third Kurt G{\"o}del Colloquium, KGC{\textquoteright}93, Brno, Czech Republic, August 24{\textendash}27, 1993, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {713},
year = {1993},
pages = {71-82},
publisher = {Springer},
organization = {Springer},
abstract = {We discuss the logics of the operators {\textquoteleft}{\textquoteleft}$p$~is a proof of~$A${\textquoteright}{\textquoteright} and {\textquoteleft}{\textquoteleft}$p$~is a proof containing~$A${\textquoteright}{\textquoteright} for the standard G{\"o}del proof predicate in Peano Arithmetic. Decidabillty and arithmetical completeness of these logics are proved. We use the same semantics as for the Provability Logic where the operator {\textquoteleft}{\textquoteleft}$A$~is provable{\textquoteright}{\textquoteright} is studied.},
doi = {10.1007/BFb0022556},
author = {Sergei Artemov and Tyko Strassen},
editor = {Georg Gottlob and Alexander Leitsch and Daniele Mundici}
}
@article {1524,
title = {The Basic Logic of Proofs},
year = {1992},
publisher = {Institut f{\"u}r Informatik und angewandte Mathematik},
abstract = {Propositional Provability Logic was axiomatized in~[Sol76]. This logic describes the behaviour of the arithmetical operator {\textquoteleft}{\textquoteleft}$y$~is provable{\textquoteright}{\textquoteright}. The aim of the current paper is to provide propositional axiomatizations of the predicate {\textquoteleft}{\textquoteleft}$x$~is a proof of~$y${\textquoteright}{\textquoteright} by means of modal logic, with the intention of meeting some of the needs of computer science.},
url = {https://www.iam.unibe.ch/de/forschung/publikationen/techreports/1992/iam-92-018},
author = {Sergei Artemov and Tyko Strassen}
}