@inbook{jae18,
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},
pdf = {https://home.inf.unibe.ch/ltg/publications/2018/jae18.pdf},
author = {Gerhard J{\"a}ger}
}
@techreport{Pro17,
author = {Dieter Probst},
title = {A modular ordinal analysis of metapredicative subsystems of second order arithmetic},
institution = {Universit{\"a}t Bern},
type = {Habilitationsschrift},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2017/pro17.pdf},
year = 2017
}
@inbook{sdo17a,
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{\textendash}500},
publisher = {Springer International Publishing},
organization = {Springer International Publishing},
address = {Cham},
isbn = {978-3-319-61581-3},
pdf = {https://home.inf.unibe.ch/ltg/publications/2017/sdo17a.pdf},
author = {Nenad Savi{\'c} and Doder, Dragan and Ognjanovi{\'c}, Zoran}
}
@article{sdo17b,
title = {Logics with lower and upper probability operators},
journal = {International Journal of Approximate Reasoning},
volume = {88},
year = {2017},
pages = {148 - 168},
issn = {0888-613X},
pdf = {https://home.inf.unibe.ch/ltg/publications/2017/sdo17b.pdf},
author = {Nenad Savi{\'c} and Dragan Doder and Zoran Ognjanovi{\'c}}
}
@conference{bgs17,
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},
pdf = {https://home.inf.unibe.ch/ltg/publications/2017/bgs17.pdf},
author = {Bucheli, Samuel and Ghari, Meghdad and Studer, Thomas},
editor = {Ghosh, Sujata and Ramanujam, R.}
}
@phdthesis{mar17,
title = {Contributions to Intuitionistic Epistemic Logic},
year = {2017},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2017/mar17.pdf},
author = {Michel Marti}
}
@article{best16,
title = {Ramsey'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},
pdf = {https://home.inf.unibe.ch/ltg/publications/2016/best16.pdf},
author = {Berardi, S. and Silvia Steila}
}
@conference{fsy17,
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{\textendash}273},
doi = {10.1007/978-3-319-55911-7_19},
pdf = {https://home.inf.unibe.ch/ltg/publications/2017/fsy17.pdf},
author = {Emanuele Frittaion and Silvia Steila and Keita Yokoyama},
editor = {T. V. Gopal and Gerhard J{\"a}ger and Silvia Steila}
}
@article{mast16,
title = {Intuitionistic modal logic made explicit},
year = {2016},
journal = {IfCoLog Journal of Logics and their Applications},
volume = {3},
number = {5},
pages = {877-901},
pdf = {https://home.inf.unibe.ch/ltg/publications/2016/mast16.pdf},
author = {Michel Marti and Thomas Studer},
abstract = {The logic of proofs of Heyting arithmetic includes explicit
justifications for all admissible rules of intuitionistic logic in order to
satisfy completeness with respect to provability semantics. We study the
justification logic iJT4, which does not have these additional justification
terms. We establish that iJT4 is complete with respect to modular models,
which provide a Kripke-style semantics, and that there is a realization
of intuitionistic S4 into iJT4. Hence iJT4 can be seen as an explicit
version of intuitionistic S4.}
}
@article{styo16.pdf,
title = {Reverse mathematical bounds for the Termination Theorem },
journal = {Annals of Pure and Applied Logic },
volume = {167},
number = {12},
pages = {1213 - 1241},
year = {2016},
note = {},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2016.06.001},
url = {//www.sciencedirect.com/science/article/pii/S0168007216300860},
author = {Silvia Steila and Keita Yokoyama},
keywords = {Reverse Mathematics},
keywords = {Ramsey's Theorem},
keywords = {Termination Theorem},
keywords = {Paris Harrington's Theorem },
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'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's Termination Theorem we can extract
some information about termination bounds. }
}
@conference{jmidk16,
title = {A canonical model construction for intuitionistic distributed knowledge},
booktitle = {Advances in Modal Logic 2016},
year = {2016},
publisher = {College Publications},
organization = {College Publications},
pdf = {https://home.inf.unibe.ch/ltg/publications/2016/jmidk16.pdf},
author = {Gerhard J{\"a}ger and Michel Marti}
}
@article{jae15,
title = {Relativizing operational set theory},
journal = {The Bulletin of Symbolic Logic},
year = {2016},
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-
eoretically equivalent to the well-known theory KPi for a recursively inaccessible universe.},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/jae15.pdf},
author = {Gerhard J{\"a}ger}
}
@article{kust16,
author = {Kuznets, Roman and Studer, Thomas},
title = {Weak arithmetical interpretations for the Logic of Proofs},
volume = {24},
number = {3},
pages = {424-440},
year = {2016},
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.},
pdf = {https://home.inf.unibe.ch/ltg/publications/2016/kust16.pdf},
journal = {Logic Journal of IGPL}
}
@book{kastrst16,
title = {Advances in Proof Theory},
editor = {Reinhard Kahle and Thomas Strahm and Thomas Studer},
isbn = {9783319291987},
series = {Progress in Computer Science and Applied Logic},
volume = {28},
year = {2016},
publisher = {Springer International Publishing}
}
@book{prob16,
title = {Concepts of Proof in Mathematics, Philosophy, and Computer Science},
editor = {Probst, Dieter and Schuster, Peter},
isbn = {9781501510809},
series = {Ontos Mathematical Logic},
volume = {6},
year = {2016},
publisher = {Walter De Gruyter Incorporated}
}
@phdthesis{kokphd16,
title = {Uncertain Reasoning in Justification Logic},
year = {2016},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2016/kokphd16.pdf},
author = {Ioannis Kokkinis}
}
@phdthesis{ran15,
title = {From a Flexible Type System to Metapredicative Wellordering Proofs},
year = {2015},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/ran15.pdf},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
author = {Ranzi, Florian}
}
@book{sost15,
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},
editor = {Giovanni Sommaruga and Thomas Strahm}
}
@techreport{stu16.pdf,
author = {Thomas Studer},
year = {2005},
institution = {Universit{\"a}t Bern},
title = {Papers in Explicit Mathematics}
}
@inproceedings{kos16,
author = {Kokkinis, Ioannis and Ognjanovi\'{c}, Zoran and Studer, Thomas},
title = {Probabilistic Justification Logic},
editor = {Artemov, Sergei and Nerode, Anil},
booktitle = {Logical Foundations of Computer Science - International Symposium, {LFCS} 2016, Deerfield Beach, FL, USA, January 4-7, 2016. Proceedings},
pages = {174--186},
series = {Lecture Notes in Computer Science},
pdf = {https://home.inf.unibe.ch/ltg/publications/2016/kos16.pdf},
volume = {9537},
publisher = {Springer},
year = {2016}
}
@inproceedings{kok16,
author = {Ioannis Kokkinis},
title = {The Complexity of Non-Iterated Probabilistic Justification Logic},
booktitle = {Foundations of Information and Knowledge Systems - 9th International Symposium, FoIKS 2016, Linz, Austria, March 7-11, 2016. Proceedings},
pages = {292--310},
editor = {Marc Gyssens and Guillermo Ricardo Simari},
series = {Lecture Notes in Computer Science},
volume = {9616},
publisher = {Springer},
year = {2016},
pdf = {https://home.inf.unibe.ch/ltg/publications/2016/kok16.pdf}
}
@inproceedings{ks16,
author = {Kokkinis, Ioannis and Studer, Thomas},
title = {Cyclic Proofs for Linear Temporal Logic},
editor = {Probst, Dieter and Schuster, Peter},
volume = {6},
series = {Ontos Mathematical Logic},
publisher = {De Gruyter},
booktitle = {Concepts of Proof in Mathematics, Philosophy, and Computer Science},
isbn = {978-1-5015-0262-0},
year = {2016},
pdf = {https://home.inf.unibe.ch/ltg/publications/2016/ks16.pdf}
}
@incollection{bjs15,
volume = {6},
month = {January},
author = {Ulrik Torben Buchholtz and Gerhard J{\"a}ger and Thomas Adrian Strahm},
series = {Ontos Mathematical Logic},
booktitle = {Concepts of Proof in Mathematics, Philosophy, and ComputerScience},
editor = {Dieter Probst and Peter Schuster},
title = {Theories of proof-theoretic strength {$\psi$}({$\Gamma$}?+1)},
publisher = {De Gruyter},
year = {2016},
journal = {Ontos Mathematical Logic},
isbn = {978-1-5015-0263-7},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/bjs15.pdf}
}
@article{ebat15,
volume = {585},
month = {June},
author = {Sebastian Eberhard},
title = {Applicative theories for logarithmic complexity classes},
publisher = {Elsevier},
journal = {Theoretical Computer Science},
pages = {115--135},
year = {2015},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/ebat15.pdf},
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's famous two-sorted algebra B for polynomial
time [4]. The second theory describes logarithmic space by
formalising concatenation- and sharply bounded recursion.
All theories contain the predicates WW representing words,
and VV representing temporary inaccessible words. They are
inspired by Cantini's theories [6] formalising B.}
}
@article{kmos15,
volume = {23},
number = {4},
month = {June},
author = {Ioannis Kokkinis and Petar Maksimovi{\'c} and
Zoran Ognjanovi{\'c} and Thomas Studer},
title = {First steps towards probabilistic justification logic},
publisher = {Oxford University Press},
year = {2015},
journal = {Logic Journal of IGPL},
pages = {662--687},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/kmos15.pdf},
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.}
}
@phdthesis{wer15,
month = {March},
title = {Controlled Query Evaluation in General Semantics with
Incomplete Information},
school = {Institut f{\"u}r Informatik und angewandte Mathematik},
author = {Johannes Martin Werner and T. Studer},
year = {2015},
note = {ISBN 978-1-326-21681-8},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/wer15.pdf}
}
@article{fkm15,
volume = {166},
number = {3},
month = {March},
author = {Melvin Fitting and Roman Kuznets},
title = {Modal interpolation via nested sequents},
publisher = {Elsevier},
year = {2015},
journal = {Annals of pure and applied logic},
pages = {274--305},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/fkm15.pdf},
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.}
}
@article{sat15a,
volume = {54},
number = {1-2},
author = {Kentaro Sato},
title = {Full and hat inductive definitions are equivalent in NBG},
publisher = {Springer},
journal = {Archive for Mathematical Logic},
pages = {75--112},
year = {2015},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/sat15a.pdf},
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
{$\Delta$}10{$\backslash$}bf-LFP and
{$\Delta$}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 {$\Delta$}n+20{$\backslash$}bf-LFP and
{$\Delta$}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).}
}
@article{sz14,
volume = {166},
number = {2},
author = {Kentaro Sato and Rico Zumbrunnen},
title = {A new model construction by making a detour
via intuitionistic theories I: Operational set
theory without choice is
{$\Pi$}1-equivalent to KP},
publisher = {Elsevier},
journal = {Annals of pure and applied logic},
pages = {121--186},
year = {2015},
pdf = {https://home.inf.unibe.ch/ltg/publications/2014/sz14.pdf},
abstract = {We introduce a version of operational set theory,
OST?, without a choice operation, which has a
machinery for
{$\Delta$}0{$\Delta$}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'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's classical realisability model.}
}
@article{sat15b,
volume = {166},
number = {7-8},
author = {Kentaro Sato},
title = {A new model construction by making a detour via
intuitionistic theories II: Interpretability
lower bound of Feferman's explicit mathematics T0},
publisher = {Elsevier},
journal = {Annals of pure and applied logic},
pages = {800--835},
year = {2015},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/sat15b.pdf},
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
{$\Sigma$}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.}
}
@incollection{esu15,
volume = {36},
author = {Sebastian Eberhard and Thomas Adrian Strahm},
series = {Logic, Epistemology, and the Unity of Science},
booktitle = {Unifying the Philosophy of Truth},
editor = {Theodora Achourioti and Henri Galinon and
Jos{\'e} Mart{\'i}nez Fern{\'a}ndez and
Kentaro Fujimoto},
address = {Dordrecht},
title = {Unfolding Feasible Arithmetic and Weak Truth},
publisher = {Springer Netherlands},
year = {2015},
pages = {153--167},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/esu15.pdf},
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).}
}
@article{jmick15,
title = {Intuitionistic common knowledge or belief},
author = {Gerhard J{\"a}ger and Michel Marti},
publisher = {Elsevier},
year = {2016},
journal = {Journal of applied logic},
pdf = {https://home.inf.unibe.ch/ltg/publications/2015/jmick15.pdf},
abstract = {Starting off from the usual language of modal logic
for multi-agent systems dealing with the agents?
knowledge/belief and common knowledge/belief we
define so-called epistemic Kripke structures for intu-
itionistic (common) knowledge/belief. Then we
introduce corresponding deductive systems and show
that they are sound and complete with respect to
these semantics.}
}
@article{bl08,
author = {Br\"unnler, Kai and Lange, Martin},
title = {Cut-free sequent systems for temporal logic},
journal = {Journal of Logic and Algebraic Programming},
volume = 76,
number = 2,
pages = {216-225},
doi = {10.1016/j.jlap.2008.02.004},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/bl08.pdf},
year = 2008
}
@inproceedings{bks10a,
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
title = {Two Ways to Common Knowledge},
booktitle = {Proceedings of the 6th~Workshop on {M}ethods for
{Modalities} ({M4M--6~2009}), {C}openhagen, {D}enmark,
12--14 {N}ovember 2009},
editor = {Thomas Bolander and Torben Bra{\"{u}}ner},
number = {262},
series = {Electronic Notes in Theoretical Computer Science},
pages = {83--98},
publisher = {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.},
doi = {10.1016/j.entcs.2010.04.007},
keywords = {justification logics, common knowledge, proof theory},
month = may,
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/bks10a.pdf},
year = 2010
}
@article{tup03,
author = {Sergei Tupailo},
title = {Realization of constructive set theory into explicit
mathematics: a lower bound for impredicative {M}ahlo
universe},
journal = {Annals of Pure and Applied Logic},
volume = {120},
number = {},
pages = {165{--}196},
ps = {https://home.inf.unibe.ch/ltg/publications/2003/tup03.ps},
year = 2003
}
@mastersthesis{kra06,
author = {J{\"u}rg Kr{\"a}henb{\"u}hl},
title = {Explicit Mathematics with Positive Existential
Comprehension and Join},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/kra06.pdf},
year = 2006
}
@article{sav12,
title = {{Product-free Lambek calculus is NP-complete}},
journal = {Annals of Pure and Applied Logic},
volume = 163,
number = 7,
pages = {775--788},
year = 2012,
note = {The Symposium on Logical Foundations of
Computer Science 2009},
issn = {0168-0072},
doi = {10.1016/j.apal.2011.09.017},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/sav12.pdf},
author = {Yury Savateev}
}
@article{sav13a,
author = {Yury Savateev},
title = {{Proof Internalization for Generalized Frege Systems
for Classical Logic}},
journal = {Annals of Pure and Applied Logic},
year = 2014,
number = {1},
pages = {340--356},
volume = {165},
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/sav13a.pdf},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.07.017},
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.}
}
@inproceedings{ste06,
author = {David Steiner},
title = {A system for consistency preserving belief change},
booktitle = {Proceedings of Rationality and Knowledge},
editor = {Sergei Artemov and Rohit Parikh},
series = {18th European Summer School of Logic, Language and
Information},
pages = {133{--}144},
publisher = {Association for Logic, Language and Information},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/ste06.pdf},
year = 2006
}
@article{str02,
author = {Thomas Strahm},
title = {Wellordering proofs for metapredicative {M}ahlo},
journal = {The Journal of Symbolic Logic},
volume = {67},
number = {1},
pages = {260{--}278},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/str02.pdf},
year = 2002
}
@inproceedings{hjss95a,
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan
Schwendimann and Michael Seyfried},
title = {Propositional logics on the computer},
booktitle = {Proceedings of Theorem Proving with Analytic Tableaux
and Related Methods},
editor = {Peter Baumgartner and Reiner H{\"a}hnle and Joachim
Posegga},
volume = {918},
series = {Lecture Notes in Computer Science},
pages = {310{--}323},
publisher = {Springer},
ps = {https://home.inf.unibe.ch/ltg/publications/1995/hjss95a.ps},
year = 1995
}
@mastersthesis{due05,
author = {Michael D{\"u}rig},
title = {$\mathcal{PALC}$: Extending $\mathcal{ALC}$ {AB}oxes
with Probabilities},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/due05.pdf},
year = 2005
}
@techreport{stu99,
author = {Thomas Studer},
title = {A semantics for $\lambda^{\{ \}}_{\mathsf{str}}$: a
calculus with overloading and late-binding},
institution = {Universit{\"a}t Bern},
number = {IAM{--}99{--}004},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
ps = {https://home.inf.unibe.ch/ltg/publications/1999/stu99.ps},
year = 1999
}
@techreport{as93a,
author = {Sergei Artemov and Tyko Strassen},
title = {Functionality in the Basic Logic of Proofs},
institution = {Institut f{\"u}r Informatik und angewandte Mathematik},
number = {iam--93--004},
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 ``$x$~is a proof of~$y$'' 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.},
pdf = {http://www.iam.unibe.ch/publikationen/techreports/1993/iam-93-004},
year = 1993
}
@inproceedings{ss05,
author = {Kilian Stoffel and Thomas Studer},
title = {Provable data privacy},
booktitle = {Proceedings of 16th International Conference on
Database and Expert Systems Applications},
editor = {Kim Viborg Andersen and John K. Debenham and Roland
Wagner},
volume = {3588},
series = {Lecture Notes in Computer Science},
pages = {324{--}332},
publisher = {Springer},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/ss05.pdf},
year = 2005
}
@article{jks01,
author = {Gerhard J{\"a}ger and Reinhard Kahle and Thomas Studer},
title = {Universes in explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {109},
number = {3},
pages = {141{--}162},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/jks01.pdf},
year = 2001
}
@article{ks06,
author = {Mathis Kretz and Thomas Studer},
title = {Deduction chains for common knowledge},
journal = {Journal of Applied Logic},
volume = {4},
number = {3},
pages = {331{--}357},
doi = {10.1016/j.jal.2005.06.011},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/ks06.pdf},
year = 2006
}
@inproceedings{mm14,
author = {Marti, Michel and Metcalfe, George},
title = {{A Hennessy-Milner Property for Many-Valued Modal
Logics}},
year = 2014,
booktitle = {Advances in Modal Logic},
volume = 10,
pages = {407--420},
publisher = {College Publications},
editor = {{Rajeev Goré and Barteld Kooi and and Agi Kurucz}},
pdf = {https://home.inf.unibe.ch/ltg/publications/2014/mm14.pdf}
}
@article{sat12,
author = {Sato, Kentaro},
title = {Relative predicativity and dependent recursion in
second-order set theory and higher-order theories},
journal = {The Journal of Symbolic Logic},
volume = 79,
issue = 03,
month = {September},
year = 2014,
issn = {1943-5886},
pages = {712--732},
doi = {10.1017/jsl.2014.28},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/sat12.pdf}
}
@article{rs13,
author = {Ranzi, Florian and Strahm, Thomas},
title = {A note on the theory $\mathsf{SID}_{{<}\omega}$ of
stratified induction},
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/rs13.pdf},
journal = {Mathematical Logic Quarterly},
volume = 60,
number = 6,
issn = {1521-3870},
doi = {10.1002/malq.201300063},
pages = {487--497},
year = 2014
}
@article{jz14,
author = {Gerhard J{\"a}ger and Rico Zumbrunnen},
title = {{Explicit mathematics and operational set theory:
some ontological comparisons}},
journal = {The Bulletin of Symbolic Logic},
volume = {20},
issue = {03},
month = {September},
year = {2014},
issn = {1943-5894},
pages = {275--292},
numpages = {18},
doi = {10.1017/bsl.2014.21},
pdf = {https://home.inf.unibe.ch/ltg/publications/2014/jz14.pdf}
}
@article{sw14,
author = {Thomas Studer and Johannes Werner},
title = {{Censors for Boolean Description Logic}},
journal = {Transactions on Data Privacy},
year = 2014,
volume = 7,
issue = 3,
pages = {223--252},
issn = {1888-5063},
pdf = {https://home.inf.unibe.ch/ltg/publications/2014/sw14.pdf}
}
@article{sat14,
author = {Sato, Kentaro},
title = {{Forcing for Hat Inductive Definitions in Arithmetic
-- One of the Simplest Applications of Forcing --}},
journal = {Mathematical Logic Quarterly},
volume = 60,
number = {4-5},
issn = {1521-3870},
doi = {10.1002/malq.201300044},
pages = {314--318},
year = 2014,
pdf = {https://home.inf.unibe.ch/ltg/publications/2014/sat14.pdf},
abstract = {By forcing, we give a direct interpretation of
$\widehat{\mathsf{ID}}_\omega$ into Avigad's
$\mathsf{FP}$. To the best of the author's
knowledge, this is one of the simplest applications
of forcing to ``real problems''.}
}
@article{fs14,
author = {Dandolo Flumini and Kentaro Sato},
title = {{From hierarchies to well-foundedness}},
journal = {Archive for Mathematical Logic},
pdf = {https://home.inf.unibe.ch/ltg/publications/2014/fs14.pdf},
year = 2014,
issn = {0933-5846},
volume = 53,
number = {7--8},
doi = {10.1007/s00153-014-0392-9},
publisher = {Springer Berlin Heidelberg}
}
@article{jae13,
author = {J{\"a}ger, Gerhard},
title = {Operational closure and stability},
journal = {Annals of Pure and Applied Logic},
volume = 164,
number = {7–8},
pages = {813 - 821},
year = 2013,
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.01.004},
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/jae13.pdf},
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.}
}
@inproceedings{jz12,
author = {J{\"a}ger, Gerhard and Zumbrunnen, Rico},
title = {{About the Strength of Operational Regularity}},
pages = {305{--}324},
editor = {Ulrich Berger and Hannes Diener and Peter Schuster
and Monika Seisenberger},
booktitle = {Logic, Construction, Computation},
year = {2012},
publisher = {Ontos Verlag},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/jz12.pdf}
}
@inproceedings{weh07a,
author = {Ricardo Wehbe},
title = {Computing with common knowledge},
booktitle = {Proceedings of Artificial Intelligence and Soft
Computing},
editor = {Angel P. del Pobil},
pages = {45{--}50},
publisher = {ACTA Press},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/weh07a.pdf},
year = 2007
}
@inproceedings{str00a,
author = {Thomas Strahm},
title = {Autonomous fixed point progressions and fixed point
transfinite recursion},
booktitle = {Proceedings of Logic Colloquium '98},
editor = {Samuel S. Buss and Petr Hajek and Pavel Pudlak},
volume = {13},
series = {Association of Symbolic Logic Lecture Notes in Logic},
pages = {449{--}464},
publisher = {AK Peters},
pdf = {https://home.inf.unibe.ch/ltg/publications/2000/str00a.pdf},
year = 2000
}
@phdthesis{pro05b,
author = {Dieter Probst},
title = {Pseudo-Hierarchies in Admissible Set Theory without
Foundation and Explicit Mathematics},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/pro05b.pdf},
year = 2005
}
@article{kuz10,
author = {Roman Kuznets},
title = {Self-Referential Justifications in Epistemic Logic},
journal = {Theory of Computing Systems},
volume = {46},
number = {4},
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.},
doi = {10.1007/s00224-009-9209-3},
keywords = {self-referentiality, justification logic, epistemic
modal logic, Logic of Proofs},
month = may,
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/kuz10.pdf},
year = 2010
}
@inproceedings{bh98b,
author = {Peter Balsiger and Alain Heuerding},
title = {{L}ogics {W}orkbench 1.0},
booktitle = {Proceedings of Tableaux '98},
editor = {Harrie C. M. de Swart},
volume = {1397},
series = {Lecture Notes in Computer Science},
pages = {35{--}37},
publisher = {Springer},
year = 1998
}
@article{ss09a,
author = {Daria Spescha and Thomas Strahm},
title = {Elementary explicit types and polynomial time
operations},
journal = {Mathematical Logic Quarterly},
volume = {55},
number = {3},
pages = {245 --258},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/ss09a.pdf},
year = 2009
}
@mastersthesis{pro99,
author = {Probst, Dieter},
title = {Dependent Choice in Explicit Mathematics},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/1999/pro99.pdf},
year = 1999
}
@article{rue02,
author = {Christian R{\"u}ede},
title = {Transfinite dependent choice and $\omega$-model
reflection},
journal = {The Journal of Symbolic Logic},
volume = {67},
number = {3},
pages = {1153{--}1168},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/rue02.pdf},
year = 2002
}
@article{heu96,
author = {Alain Heuerding},
title = {{LWB}theory: information about some propositional
logics via the {WWW}},
journal = {Journal of the Interest Group in Pure and Applied
Logic},
volume = {4},
number = {4},
pages = {196{--}174},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/heu96.ps},
year = 1996
}
@phdthesis{wir05,
author = {Marc Wirz},
title = {Wellordering Two Sorts: A Slow-Growing Proof Theory
for Variable Separation},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/wir05.pdf},
year = 2005
}
@article{bhs00,
author = {Peter Balsiger and Alain Heuerding and Stefan
Schwendimann},
title = {A benchmark method for the propositional modal logics
{K}, {KT}, {S4}},
journal = {Journal of Automated Reasoning},
volume = {24},
number = {3},
pages = {297{--}317},
pdf = {https://home.inf.unibe.ch/ltg/publications/2000/bhs00.pdf},
year = 2000
}
@article{ghh97,
author = {Rajeev Gor{\'e} and Wolfgang Heinle and Alain
Heuerding},
title = {Relations between propositional normal modal logics:
an overview},
journal = {Journal of Logic and Computation},
volume = {7},
number = {5},
pages = {649{--}658},
ps = {https://home.inf.unibe.ch/ltg/publications/1997/ghh97.ps},
year = 1997
}
@inproceedings{bm08,
author = {Br{\"u}nnler, Kai and McKinley, Richard},
title = {An Algorithmic Interpretation of a Deep Inference
System},
booktitle = {LPAR 2008},
editor = {Cervesato, I. and Veith, H. and Voronkov, A.},
volume = {5330},
series = {Lecture Notes in Computer Science},
pages = {482---496},
publisher = {Springer-Verlag},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/bm08.pdf},
year = 2008
}
@inproceedings{hs96a,
author = {Alain Heuerding and Stefan Schwendimann},
title = {On the modal logic {K} plus theories},
booktitle = {Proceedings of Computer Science Logic '95},
editor = {Hans Kleine B{\"u}ning},
volume = {1092},
series = {Lecture Notes in Computer Science},
pages = {308{--}319},
publisher = {Springer},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/hs96a.ps},
year = 1996
}
@article{af09a,
author = {Luca Alberucci and Alessandro Facchini},
title = {On modal $\mu$-calculus and {G}{\"o}del-{L}{\"o}b
logic},
journal = {Studia Logica},
volume = {91},
pages = {145-169},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/af09a.pdf},
year = 2009
}
@inproceedings{hsz96,
author = {Alain Heuerding and Michael Seyfried and Heinrich
Zimmermann},
title = {Efficient loop-check for backward proof search in some
non-classical propositional logics},
booktitle = {Proceedings of Tableaux '96},
editor = {Pierangelo Miglioli and Ugo Moscato and Daniele
Mundici and Mario Ornaghi},
volume = {1071},
series = {Lecture Notes in Computer Science},
pages = {210{--}225},
publisher = {Springer},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/hsz96.ps},
year = 1996
}
@article{js00,
author = {Gerhard J{\"a}ger and Thomas Strahm},
title = {Fixed point theories and dependent choice},
journal = {Archive for Mathematical Logic},
volume = {39},
number = {7},
pages = {493{--}508},
ps = {https://home.inf.unibe.ch/ltg/publications/2000/js00.ps},
year = 2000
}
@inproceedings{bs09a,
author = {Kai Br{\"u}nnler and Thomas Studer},
title = {Syntactic cut-elimination for common knowledge},
booktitle = {Proceedings of {M}ethods for {M}odalities {M}4{M}5},
editor = {Areces, C. and Demri, S.},
volume = {231},
series = {ENTCS},
pages = {227--240},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2009.02.038},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/bs09a.pdf},
year = 2009
}
@article{js95a,
author = {Gerhard J{\"a}ger and Thomas Strahm},
title = {Second order theories with ordinals and elementary
comprehension},
journal = {Archive for Mathematical Logic},
volume = {34},
number = {6},
pages = {345{--}375},
ps = {https://home.inf.unibe.ch/ltg/publications/1995/js95a.ps},
year = 1995
}
@phdthesis{stu01c,
author = {Thomas Studer},
title = {Object-Oriented Programming in Explicit Mathematics:
Towards the Mathematics of Objects},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/stu01c.pdf},
year = 2001
}
@article{kah98,
author = {Reinhard Kahle},
title = {{F}rege structures for partial applicative theories},
journal = {Journal of Logic and Computation},
volume = {8},
number = {5},
pages = {683{--}700},
doi = {10.1093/logcom/9.5.683},
url = {http://dx.doi.org/10.1093/logcom/9.5.683},
year = 1998
}
@article{bks11a,
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
title = {Justifications for Common Knowledge},
journal = {Journal of Applied Non-classical Logics},
volume = {21},
number = {1},
pages = {35-60},
doi = {10.3166/JANCL.21.35-60},
editor = {Valentin Goranko and Wojtek Jamroga},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/bks11a.pdf},
year = 2011
}
@article{aj05,
author = {Luca Alberucci and Gerhard J{\"a}ger},
title = {About cut elimination for logics of common knowledge},
journal = {Annals of Pure and Applied Logic},
volume = {133},
number = {1{--}3},
pages = {73{--}99},
doi = {10.1016/j.apal.2004.10.004},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/aj05.pdf},
year = 2005
}
@techreport{cfh97b,
author = {Edmund M. Clarke and Masayuki Fujita and Wolfgang
Heinle},
title = {Hybrid spectral transform diagrams},
institution = {Carnegie Mellon University},
number = {CMU{--}CS{--}97{--}149},
address = {Department of Computer Science},
year = 1997
}
@inproceedings{bru06b,
author = {Kai Br{\"u}nnler},
title = {Deep inference and its normal form of derivations},
booktitle = {Proceedings of Computability in Europe},
editor = {Arnold Beckmann and Ulrich Berger and Benedikt
L{\"o}we and John V. Tucker},
volume = {3988},
series = {Lecture Notes in Computer Science},
pages = {65{--}74},
publisher = {Springer},
doi = {10.1007/11780342_7},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/bru06b.pdf},
year = 2006
}
@inproceedings{sch98a,
author = {Stefan Schwendimann},
title = {A new one-pass tableau calculus for $\mathsf{PLTL}$},
booktitle = {Proceedings of Tableaux '98},
editor = {Harrie C. M. de Swart},
volume = {1397},
series = {Lecture Notes in Computer Science},
pages = {277{--}292},
publisher = {Springer},
ps = {https://home.inf.unibe.ch/ltg/publications/1998/sch98a.ps},
year = 1998
}
@article{js02b,
author = {Gerhard J{\"a}ger and Thomas Studer},
title = {Extending the system $\mathsf{T}_{0}$ of explicit
mathematics: the limit and {M}ahlo axioms},
journal = {Annals of Pure and Applied Logic},
volume = {114},
number = {1{--}3},
pages = {79{--}101},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/js02b.pdf},
year = 2002
}
@article{str96b,
author = {Thomas Strahm},
title = {Partial applicative theories and explicit
substitutions},
journal = {Journal of Logic and Computation},
volume = {6},
number = {1},
pages = {55{--}77},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/str96b.ps},
year = 1996
}
@inproceedings{ss07a,
author = {David Steiner and Thomas Studer},
title = {Total public announcements},
booktitle = {Proceedings of Logical Foundations of Computer Science},
editor = {Sergei Artemov and Anil Nerode},
volume = {4514},
series = {Lecture Notes in Computer Science},
pages = {498{--}511},
publisher = {Springer},
doi = {10.1007/978-3-540-72734-7_35},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/ss07a.pdf},
year = 2007
}
@mastersthesis{sto10,
author = {Stolz, Manuela Claudia},
title = {Verification of {W}orkflow {C}ontrol-{F}low {P}atterns
with the {SPIN} {M}odel {C}hecker},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
year = 2010
}
@article{jae07,
author = {Gerhard J{\"a}ger},
title = {On {F}eferman's operational set theory $\mathsf{OST}$},
journal = {Annals of Pure and Applied Logic},
volume = {150},
number = {1{--}3},
pages = {19{--}39},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/jae07.pdf},
year = 2007
}
@mastersthesis{lin08,
author = {Liniger, Simone},
title = {The {B}asic {F}easible {F}unctionals in {B}ounded
{A}rithmetic},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/lin08.pdf},
year = 2008
}
@article{js05,
author = {Gerhard J{\"a}ger and Thomas Strahm},
title = {Reflections on reflections in explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {136},
number = {1{--}2},
pages = {116{--}133},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/js05.pdf},
year = 2005
}
@incollection{jae97b,
author = {Gerhard J{\"a}ger},
title = {Some proof theory of first order logic programming},
booktitle = {Logic of Computation},
publisher = {Springer},
editor = {Helmut Schwichtenberg},
volume = {157},
series = {{NATO} Science Series},
pages = {201{--}228},
year = 1997
}
@inproceedings{as93c,
author = {Sergei Artemov and Tyko Strassen},
title = {The Logic of the {G\"{o}}del Proof Predicate},
booktitle = {Computational Logic and Proof Theory, Third {K}urt
{G\"{o}}del {C}olloquium, {KGC}'93, {B}rno, {C}zech
{R}epublic, {A}ugust 24--27, 1993, Proceedings},
editor = {Georg Gottlob and Alexander Leitsch and Daniele
Mundici},
volume = 713,
series = {Lecture Notes in Computer Science},
pages = {71--82},
publisher = {Springer},
abstract = {We discuss the logics of the operators ``$p$~is a
proof of~$A$'' and ``$p$~is a proof containing~$A$''
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
``$A$~is provable'' is studied.},
doi = {10.1007/BFb0022556},
year = 1993
}
@techreport{str01,
author = {Thomas Strahm},
title = {Proof-theoretic contributions to explicit mathematics},
institution = {Universit{\"a}t Bern},
type = {Habilitationsschrift},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/str01.pdf},
year = 2001
}
@article{fs00,
author = {Solomon Feferman and Thomas Strahm},
title = {The unfolding of non-finitist arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {104},
number = {1{--}3},
pages = {75{--}96},
ps = {https://home.inf.unibe.ch/ltg/publications/2000/fs00.ps},
year = 2000
}
@phdthesis{rue00,
author = {Christian R{\"u}ede},
title = {Metapredicative Subsystems of Analysis},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2000/rue00.pdf},
year = 2000
}
@article{af09b,
author = {Luca Alberucci and Alessandro Facchini},
title = {The modal $\mu$-calculus hierarchy over restricted
classes of transition systems},
journal = {Journal of Symbolic Logic},
volume = {74},
number = {4},
pages = {1367--1400},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/af09b.pdf},
year = 2009
}
@techreport{kah96a,
author = {Reinhard Kahle},
title = {Universes over {F}rege Structures},
institution = {Universit{\"a}t Bern},
number = {IAM{--}96{--}010},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/kah96a.ps},
year = 1996
}
@article{stu05a,
author = {Thomas Studer},
title = {Explicit mathematics: power types and overloading},
journal = {Annals of Pure and Applied Logic},
volume = {134},
number = {2{--}3},
pages = {284{--}302},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/stu05a.pdf},
year = 2005
}
@article{hj94,
author = {Brigitte H{\"o}sli and Gerhard J{\"a}ger},
title = {About some symmetries of negation},
journal = {The Journal of Symbolic Logic},
volume = {59},
number = {2},
pages = {473{--}485},
url = {http://www.jstor.org/stable/2275401},
year = 1994
}
@article{js96,
author = {Gerhard J{\"a}ger and Thomas Strahm},
title = {Some theories with positive induction of ordinal
strength $\varphi \omega 0$},
journal = {The Journal of Symbolic Logic},
volume = {61},
number = {3},
pages = {818{--}842},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/js96.ps},
year = 1996
}
@article{ak13,
author = {Artemov, Sergei and Kuznets, Roman},
title = {{Logical Omniscience As Infeasibility}},
journal = {Annals of Pure and Applied Logic},
number = 1,
pages = {6--25},
volume = 165,
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/ak13.pdf},
year = 2014,
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.07.003},
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.}
}
@inproceedings{ak09,
author = {Artemov, Sergei and Kuznets, Roman},
title = {Logical Omniscience as a Computational Complexity
Problem},
booktitle = {Theoretical {A}spects of {R}ationality and
{K}nowledge, Proceedings of the Twelfth Conference
({TARK~2009})},
editor = {Aviad Heifetz},
pages = {14--23},
address = {Stanford University, California},
publisher = {ACM},
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},
month = jul # { 6--8,},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/ak09.pdf},
year = 2009
}
@article{jae01,
author = {Gerhard J{\"a}ger},
title = {First order theories for nonmonotone inductive
definitions: recursively inaccessible and {M}ahlo},
journal = {The Journal of Symbolic Logic},
volume = {66},
number = {3},
pages = {1073{--}1089},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/jae01.pdf},
year = 2001
}
@mastersthesis{kel02,
author = {Philipp Keller},
title = {Information Flow {--} Logics for the (R)age of
Information},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/kel02.pdf},
year = 2002
}
@inproceedings{bgk10,
author = {Kai Br{\"u}nnler and Remo Goetschi and Roman Kuznets},
title = {A Syntactic Realization Theorem for Justification
Logics},
booktitle = {Advances in Modal Logic, Volume 8},
editor = {Lev Beklemishev and Valentin Goranko and Valentin
Shehtman},
pages = {39--58},
publisher = {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'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 = {justification logic, modal logic, realization theorem,
nested sequents, positive introspection},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/bgk10.pdf},
year = 2010
}
@article{gk12,
author = {Goetschi, Remo and Kuznets, Roman},
title = {Realization for {J}ustification {L}ogics via
{N}ested {S}equents: {M}odularity through
{E}mbedding},
journal = {Annals of Pure and Applied Logic},
month = {September},
number = {9},
pages = {1271--1298},
volume = {163},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/gk12.pdf},
issn = {0168-0072},
doi = {10.1016/j.apal.2012.02.002},
url = {http://www.sciencedirect.com/science/article/pii/S0168007212000565},
year = 2012
}
@inproceedings{cfh97a,
author = {Edmund M. Clarke and Masayuki Fujita and Wolfgang
Heinle},
title = {Hybrid spectral transform diagrams},
booktitle = {Proceedings of the International Conference on
Information and Communications Security},
editor = {Yongfei Han and Tatsuaki Okamoto and Sihan Qing},
volume = {1334},
series = {Lecture Notes in Computer Science},
pages = {251{--}255},
publisher = {Springer},
year = 1997
}
@mastersthesis{bor99,
author = {Afshin D. Boroumand},
title = {Logics Workbench f{\"u}r Window System},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
year = 1999
}
@article{kah00,
author = {Reinhard Kahle},
title = {{N}-strictness in applicative theories},
journal = {Archive for Mathematical Logic},
volume = {39},
number = {2},
pages = {125{--}144},
doi = {10.1007/s001530050007},
url = {http://dx.doi.org/10.1007/s001530050007},
year = 2000
}
@phdthesis{heu98,
author = {Alain Heuerding},
title = {Sequent Calculi for Proof Search in some Modal Logics},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/1998/heu98.pdf},
year = 1998
}
@inproceedings{bs09c,
author = {Br{\"u}nnler, Kai and Stra{\ss}burger, Lutz},
title = {Modular Sequent Systems for Modal Logic},
booktitle = {Tableaux 2009},
editor = {Giese, Martin and Waaler, Arild},
volume = {5607},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
doi = {10.1007/978-3-642-02716-1_12},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/bs09c.pdf},
year = 2009
}
@phdthesis{kah97a,
author = {Reinhard Kahle},
title = {Applikative Theorien und Frege-Strukturen},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
ps = {https://home.inf.unibe.ch/ltg/publications/1997/kah97a.ps},
year = 1997
}
@article{sto07,
author = {Phiniki Stouppa},
title = {A deep inference system for the modal logic
$\mathsf{S5}$},
journal = {Studia Logica},
volume = {85},
number = {2},
pages = {199{--}214},
doi = {10.1007/s11225-007-9028-y},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/sto07.pdf},
year = 2007
}
@article{rue03b,
author = {Christian R{\"u}ede},
title = {Universes in metapredicative analysis},
journal = {Archive for Mathematical Logic},
volume = {42},
number = {2},
pages = {129{--}151},
pdf = {https://home.inf.unibe.ch/ltg/publications/2003/rue03b.pdf},
year = 2003
}
@article{bps08,
author = {Kai Br{\"u}nnler and Dieter Probst and Thomas Studer},
title = {On contraction and the modal fragment},
journal = {Mathematical Logic Quarterly},
volume = {54},
number = {4},
pages = {345--349},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/bps08.pdf},
year = 2008
}
@article{pro05a,
author = {Dieter Probst},
title = {On the relationship between fixed points and iteration
in admissible set theory without foundation},
journal = {Archive for Mathematical Logic},
volume = {44},
number = {5},
pages = {561{--}580},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/pro05a.pdf},
year = 2005
}
@article{ps11,
author = {Probst, Dieter and Strahm, Thomas},
title = {Admissible closures of polynomial time computable
arithmetic},
journal = {Archive for Mathematical Logic},
volume = {50},
number = {5-6},
pages = {643-660},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/ps11.pdf},
year = 2011
}
@techreport{alb07,
author = {Luca Alberucci},
title = {A syntactical treatment of simultaneous fixpoints in
the modal $\mu$-calculus},
institution = {Universit{\"a}t Bern},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/alb07.pdf},
year = 2007
}
@article{sz08,
author = {Strahm, Thomas and Zucker, Jeffery I},
title = {Primitive recursive selection functions for
existential assertions over abstract algebras},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
number = {2},
pages = {175-197},
abstract = {},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/sz08.pdf},
year = 2008
}
@mastersthesis{kre00,
author = {Michel Krebs},
title = {{E}inige {A}spekte der {M}odallogik $\mathsf{S5}_{n}$
mit {A}llgemeinwissen},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2000/kre00.pdf},
year = 2000
}
@article{bru06d,
author = {Kai Br{\"u}nnler},
title = {Locality for classical logic},
journal = {Notre Dame Journal of Formal Logic},
volume = {47},
number = {4},
pages = {557{--}580},
doi = {10.1305/ndjfl/1168352668},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/bru06d.pdf},
year = 2006
}
@mastersthesis{buc08,
author = {Samuel Bucheli},
title = {Explicit Mathematics with Positive Existential
Stratified Comprehension, Join and Uniform Monotone
Inductive Definitions},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/buc08.pdf},
year = 2008
}
@phdthesis{buc12,
author = {Bucheli, Samuel},
title = {{J}ustification Logics with {C}ommon {K}nowledge},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/buc12.pdf},
year = 2012
}
@phdthesis{goe12,
author = {Remo Goetschi},
title = {{O}n the {R}ealization and {C}lassification of {J}ustification {L}ogics},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/goe12.pdf},
year = 2012
}
@incollection{chs97,
author = {Edmund M. Clarke and Wolfgang Heinle and Holger
Schlingloff},
title = {Model checking},
booktitle = {Handbook of Automated Reasoning},
publisher = {Elsevier Science},
editor = {Alan Robinson and Andrei Voronkov},
pages = {1635{--}1790},
year = 1997
}
@mastersthesis{hei01,
author = {Marc Heissenb{\"u}ttel},
title = {Theories of Ordinal Strength $\varphi 2 0$ and
$\varphi 2 \varepsilon_{0}$},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/hei01.pdf},
year = 2001
}
@inproceedings{jae95,
author = {Gerhard J{\"a}ger},
title = {A deductive approach to logic programming},
booktitle = {Proof and Computation},
editor = {Helmut Schwichtenberg},
volume = {139},
series = {NATO ASI Series F},
pages = {231{--}270},
publisher = {Springer},
year = 1995
}
@article{ss11,
author = {Spescha, Daria and Strahm, Thomas},
title = {Realizability in weak systems of explicit mathematics},
journal = {Mathematical Logic Quarterly},
volume = {57},
number = {6},
pages = {551-565},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/ss11.pdf},
year = 2011
}
@article{pro06,
author = {Probst, Dieter},
title = {The proof-theoretic analysis of transfinitely iterated
quasi least fixed points},
journal = {The Journal of Symbolic Logic},
volume = {71},
number = {3},
pages = {721{--}746},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/pro06.pdf},
year = 2006
}
@incollection{mt99,
author = {Grigori Mints and Sergei Tupailo},
title = {Epsilon-substitution method for the ramified language
and ${\Delta}^{1}_{1}$-comprehension rule},
booktitle = {Logic and Foundation of Mathematics},
publisher = {Kluwer},
editor = {Andrea Cantini and Ettore Casari and Pierluigi Minari},
pages = {107{--}130},
year = 1999
}
@phdthesis{sto09,
author = {Stouppa, Phiniki},
title = {Deciding {D}ata {P}rivacy for {ALC} {K}nowledge
{B}ases},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/sto09.pdf},
year = 2009
}
@article{js95b,
author = {Gerhard J{\"a}ger and Thomas Strahm},
title = {Totality in applicative theories},
journal = {Annals of Pure and Applied Logic},
volume = {74},
number = {2},
pages = {105{--}120},
ps = {https://home.inf.unibe.ch/ltg/publications/1995/js95b.ps},
year = 1995
}
@inproceedings{jae93b,
author = {Gerhard J{\"a}ger},
title = {Some proof-theoretic aspects of logic programming},
booktitle = {Logic and Algebra of Specification},
editor = {Friedrich Ludwig Bauer and Wilfried Brauer and Helmut
Schwichtenberg},
volume = {94},
series = {Computer and Systems Sciences},
pages = {113{--}142},
publisher = {Springer},
year = 1993
}
@article{str97,
author = {Thomas Strahm},
title = {Polynomial time operations in explicit mathematics},
journal = {The Journal of Symbolic Logic},
volume = {62},
number = {2},
pages = {575{--}594},
ps = {https://home.inf.unibe.ch/ltg/publications/1997/str97.ps},
year = 1997
}
@techreport{kah95,
author = {Reinhard Kahle},
title = {Natural numbers and forms of weak induction in
applicative theories},
institution = {Universit{\"a}t Bern},
number = {IAM{--}95{--}001},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
ps = {https://home.inf.unibe.ch/ltg/publications/1995/kah95.ps},
year = 1995
}
@inproceedings{bru06c,
author = {Kai Br{\"u}nnler},
title = {Deep sequent systems for modal logic},
booktitle = {Proceedings of Advances in Modal Logic},
editor = {Guido Governatori and Ian Hodkinson and Yde Venema},
volume = {6},
pages = {107{--}119},
publisher = {College Publications},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/bru06c.pdf},
year = 2006
}
@article{fj96,
author = {Solomon Feferman and Gerhard J{\"a}ger},
title = {Systems of explicit mathematics with non-constructive
$\mu$-operator. {P}art {II}},
journal = {Annals of Pure and Applied Logic},
volume = {79},
number = {1},
pages = {37{--}52},
doi = {10.1016/0168-0072(95)00028-3},
url = {http://dx.doi.org/10.1016/0168-0072(95)00028-3},
year = 1996
}
@mastersthesis{tra09,
author = {Traber, Roger},
title = {Proof-{S}ystems for {PLTL}: {C}ycling {S}equents and
their {U}se in a {F}initization for {PLTL}},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/tra09.pdf},
year = 2009
}
@mastersthesis{zum09,
author = {Zumbrunnen, Rico},
title = {Ontological {Q}uestions about {O}perational {S}et
{T}heory},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/zum09.pdf},
year = 2009
}
@phdthesis{str96a,
author = {Thomas Strahm},
title = {On the Proof Theory of Applicative Theories},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/str96a.ps},
year = 1996
}
@inproceedings{stu05b,
author = {Thomas Studer},
title = {Relational representation of $\mathcal{ALN}$ knowledge
bases},
booktitle = {Proceedings of Multi '05},
editor = {Pedro Isa{\'i}as and Miguel B. Nunes and Antonio Palma
dos Reis},
pages = {271{--}278},
publisher = {International Association for Development of the
Information Society},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/stu05b.pdf},
year = 2005
}
@article{ks01,
author = {Reinhard Kahle and Thomas Studer},
title = {Formalizing non-termination of recursive programs},
journal = {Journal of Logic and Algebraic Programming},
volume = {49},
number = {1{--}2},
pages = {1{--}14},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/ks01.pdf},
year = 2001
}
@article{bs09b,
author = {Br\"unnler, Kai and Studer, Thomas},
title = {Syntactic cut-elimination for common knowledge},
journal = {Annals of Pure and Applied Logic},
volume = {160},
number = {1},
pages = {82-95},
doi = {10.1016/j.apal.2009.01.014},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/bs09b.pdf},
year = 2009
}
@article{tup01,
author = {Sergei Tupailo},
title = {Realization of analysis into explicit mathematics},
journal = {The Journal of Symbolic Logic},
volume = {66},
number = {4},
pages = {1848{--}1864},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/tup01.pdf},
year = 2001
}
@techreport{as92,
author = {Sergei Artemov and Tyko Strassen},
title = {{The Basic Logic of Proofs}},
institution = {Institut f{\"u}r Informatik und angewandte Mathematik},
number = {iam--92--018},
abstract = {Propositional Provability Logic was axiomatized
in~[Sol76]. This logic describes the behaviour of the
arithmetical operator ``$y$~is provable''. The aim of
the current paper is to provide propositional
axiomatizations of the predicate ``$x$~is a proof
of~$y$'' by means of modal logic, with the intention of
meeting some of the needs of computer science.},
pdf = {http://www.iam.unibe.ch/publikationen/techreports/1992/iam-92-018},
year = 1992
}
@article{ms98,
author = {Markus Marzetta and Thomas Strahm},
title = {The $\mu$ quantification operator in explicit
mathematics with universes and iterated fixed point
theories with ordinals},
journal = {Archive for Mathematical Logic},
volume = {37},
number = {5},
pages = {391{--}413},
ps = {https://home.inf.unibe.ch/ltg/publications/1998/ms98.ps},
year = 1998
}
@article{bru06a,
author = {Kai Br{\"u}nnler},
title = {Cut elimination inside a deep inference system for
classical predicate logic},
journal = {Studia Logica},
volume = {82},
number = {1},
pages = {51{--}71},
doi = {10.1007/s11225-006-6605-4},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/bru06a.pdf},
year = 2006
}
@inproceedings{stu10a,
author = {Studer, Thomas},
title = {Privacy {P}reserving {M}odules for {O}ntologies},
booktitle = {Proceedings of {P}erspectives of {S}ystem
{I}nformatics {PSI}'09},
editor = {A. Pnueli and I. Virbitskaite and A. Voronkov},
volume = {5947},
series = {Lecture Notes in Computer Science},
pages = {380{--}387},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/stu10a.pdf},
year = 2010
}
@article{stu11a,
author = {Studer, Thomas},
title = {Justification {L}ogic, {I}nference {T}racking, and {D}ata {P}rivacy},
journal = {Logic and Logical Philosophy},
volume = {20},
number = {4},
pages = {297{--}306},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/stu11a.pdf},
year = 2011
}
@inproceedings{stu11b,
author = {Studer, Thomas},
title = {An application of justification logic to protocol verification},
booktitle = {Proceedings of {C}omputational {I}ntelligence and {S}ecurity {CIS} 2011},
publisher = {IEEE},
pages = {779{--}783},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/stu11b.pdf},
year = 2011
}
@inproceedings{ms12,
author = {Mints, Grigori and Studer, Thomas},
title = {Cut-elimination for the mu-calculus with one variable},
booktitle = {Fixed {P}oints in {C}omputer {S}cience 2012},
volume = {77},
series = {EPTCS},
pages = {47{--}54},
publisher = {Open Publishing Association},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/ms12.pdf},
year = 2012
}
@mastersthesis{fab11,
author = {Daniel Fabian},
title = {Applicative theories on tree ordinal numbers},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/fab11.pdf},
year = 2011
}
@article{alb09,
author = {Luca Alberucci},
title = {Sequent calculi for the modal $\mu$-calculus over
$\mathsf{S5}$},
journal = {Journal of Logic and Computation},
note = {Published online on January 22, 2009},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/alb09.pdf},
year = 2009
}
@mastersthesis{kre02,
author = {Mathis Kretz},
title = {On the Treatment of Predicative Polymorphism in
Theories of Explicit Mathematics},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/kre02.pdf},
year = 2002
}
@inproceedings{weh06b,
author = {Ricardo Wehbe},
title = {Revising non-monotonic rule-based belief databases},
booktitle = {Proceedings of Belief Revision, Belief Merging and
Social Choice},
series = {8th Augustus De Morgan Workshop},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/weh06b.pdf},
year = 2006
}
@mastersthesis{wir99b,
author = {Marc Wirz},
title = {{C}harakterisierungen kleiner
{K}omplexit{\"a}tsklassen mittels geschichteter
{N}-{P}r{\"a}dikate},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/1999/wir99b.pdf},
year = 1999
}
@inproceedings{hs95,
author = {Wolfgang Heinle and Bernd-Holger Schlingloff},
title = {Relational semantics for modal logics},
booktitle = {Proceedings of Verification in New Orientations},
editor = {Robert Rodosek},
pages = {104-131},
publisher = {University of Maribor},
ps = {https://home.inf.unibe.ch/ltg/publications/1995/hs95.ps},
year = 1995
}
@article{bru09,
author = {Kai Br{\"u}nnler},
title = {Deep Sequent Systems for Modal Logic},
journal = {Archive for Mathematical Logic},
volume = 48,
pages = {551--577},
doi = {10.1007/s00153-009-0137-3},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/bru09.pdf},
year = 2009
}
@techreport{bru10b,
author = {Kai Br{\"u}nnler},
title = {Nested {S}equents},
institution = {Universit{\"a}t Bern},
type = {Habilitationsschrift},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
url = {http://arxiv.org/abs/1004.1845v1},
year = 2010
}
@article{gs96,
author = {Thomas Glass and Thomas Strahm},
title = {Systems of explicit mathematics with non-constructive
$\mu$-operator and join},
journal = {Annals of Pure and Applied Logic},
volume = {82},
number = {2},
pages = {193{--}219},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/gs96.ps},
year = 1996
}
@mastersthesis{bri99,
author = {Jimmy Brignioni},
title = {{K}onstruktion von {G}egenmodellen intuitionistisch
unbeweisbarer {S}equenzen},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
year = 1999
}
@article{jae97a,
author = {Gerhard J{\"a}ger},
title = {Power types in explicit mathematics?},
journal = {The Journal of Symbolic Logic},
volume = {62},
number = {4},
pages = {1142{--}1146},
url = {http://www.jstor.org/stable/2275630},
year = 1997
}
@techreport{kah97b,
author = {Reinhard Kahle},
title = {Uniform limit in explicit mathematics with universes},
institution = {Universit{\"a}t Bern},
number = {IAM{--}97{--}002},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
ps = {https://home.inf.unibe.ch/ltg/publications/1997/kah97b.ps},
year = 1997
}
@mastersthesis{bur04,
author = {Theo Burri},
title = {Weak K{\"o}nig's Lemma and Extensional Equality},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2004/bur04.pdf},
year = 2004
}
@inproceedings{ss07b,
author = {Phiniki Stouppa and Thomas Studer},
title = {A formal model of data privacy},
booktitle = {Proceedings of Perspectives of System Informatics},
editor = {Irina Virbitskaite and Andrei Voronkov},
volume = {4378},
series = {Lecture Notes in Computer Science},
pages = {401{--}411},
publisher = {Springer},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/ss07b.pdf},
year = 2007
}
@techreport{hs97,
author = {Wolfgang Heinle and Holger Schlingloff},
title = {Modal rule correspondences},
institution = {Universit{\"a}t Bern},
type = {Dagstuhl Seminar report},
number = {9403},
year = 1997
}
@incollection{jks99,
author = {Gerhard J{\"a}ger and Reinhard Kahle and Thomas Strahm},
title = {On applicative theories},
booktitle = {Logic and Foundations of Mathematics},
publisher = {Kluwer},
editor = {Andrea Cantini and Ettore Casari and Pierluigi Minari},
pages = {83{--}92},
ps = {https://home.inf.unibe.ch/ltg/publications/1999/jks99.ps},
year = 1999
}
@article{hjss96a,
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan
Schwendimann and Michael Seyfried},
title = {A logics workbench},
journal = {The European Journal on Artificial Intelligence},
volume = {9},
number = {2},
pages = {53{--}58},
year = 1996
}
@article{pro11,
author = {Probst, Dieter},
title = {The provably terminating operations of the subsystem
{PETJ} of explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {162},
pages = {934--947},
number = {11},
doi = {10.1016/j.apal.2011.04.004},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/pro11.pdf},
year = 2011
}
@inproceedings{jp04a,
author = {Gerhard J{\"a}ger and Dieter Probst},
title = {Iterating ${\Sigma}$ operations in admissible set
theory without foundation: a further aspect of
metapredicative {M}ahlo},
booktitle = {One Hundred Years of Russell's Paradox. Papers from
the 2001 Munich Russell Conference},
editor = {Godehart Link},
pages = {119{--}134},
publisher = {de Gruyter},
pdf = {https://home.inf.unibe.ch/ltg/publications/2004/jp04a.pdf},
year = 2004
}
@book{str08a,
editor = {Strahm, Thomas},
title = {G\"odel's {D}ialectica {I}nterpretation},
publisher = {Wiley},
number = {62(2)},
series = {Dialectica},
edition = {Special},
url = {http://onlinelibrary.wiley.com/doi/10.1111/dltc.2008.62.issue-2/issuetoc},
year = 2008
}
@incollection{js98,
author = {Gerhard J{\"a}ger and Robert F. St{\"a}rk},
title = {A proof-theoretic framework for logic programming},
booktitle = {Handbook of Proof Theory},
publisher = {North-Holland},
editor = {Samuel S. Buss},
pages = {639{--}682},
doi = {10.1016/S0049-237X(98)80024-4},
url = {http://dx.doi.org/10.1016/S0049-237X(98)80024-4},
year = 1998
}
@inproceedings{jks05,
author = {Gerhard J{\"a}ger and Mathis Kretz and Thomas Studer},
title = {Cut-free axiomatizations for stratified modal fixed
point logic},
booktitle = {Proceedings of Methods for Modalities 4},
editor = {Holger Schlingloff},
volume = {194},
series = {Humboldt-Universit{\"a}t Berlin Informatik-Berichte},
pages = {125{--}143},
publisher = {Humboldt-Universit{\"a}t Berlin},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/jks05.pdf},
year = 2005
}
@phdthesis{str94,
author = {Strassen, Tyko},
title = {The Basic Logic of Proofs},
school = {University of Bern},
abstract = {Propositional Provability Logic was axiomatized by
R.~M.~Solovay in~1976. This modal logic describes the
behavior of the arithmetical operator ``$A$~is
provable''. The aim of these investigations is to
provide propositional axiomatizations of the predicates
``$p$~is a proof of~$A$'', ``$p$~is a proof which
contains~$A$'' and ``$p$~is a program which
computes~$A$'' 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.},
month = apr,
url = {http://www.strassen.us/thesis.pdf},
year = 1994
}
@mastersthesis{goe08,
author = {Remo Goetschi},
title = {Polytime Functions in Two-Sorted Bounded Arithmetic},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/goe08.pdf},
year = 2008
}
@mastersthesis{spe05,
author = {Daria Spescha},
title = {{ALOE} {--} A Graphical Editor for {OWL} Ontologies},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/spe05.pdf},
year = 2005
}
@article{jks08,
author = {J{\"a}ger, Gerhard and Kretz, Mathis and Studer,
Thomas},
title = {Canonical completeness of infinitary mu},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
number = {2},
pages = {270-292},
abstract = {},
doi = {10.1016/j.jlap.2008.02.005},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/jks08.pdf},
year = 2008
}
@mastersthesis{sch03,
author = {Thomas Schweizer},
title = {Two Interpretations of $\mathsf{WKL}_{0}$ in
Subsystems of $\mathsf{PA}$},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2003/sch03.pdf},
year = 2003
}
@article{fs10,
author = {Feferman, Solomon and Strahm, Thomas},
title = {Unfolding finitist arithmetic},
journal = {Review of Symbolic Logic},
volume = {3},
number = {4},
pages = {665--689},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/fs10.pdf},
year = 2010
}
@inproceedings{kuz09b,
author = {Kuznets, Roman},
title = {A Note on the Use of Sum in the {L}ogic of {P}roofs},
booktitle = {Proceedings of the 7th~{P}anhellenic {L}ogic
{S}ymposium},
editor = {Costas Drossos and Pavlos Peppas and Constantine
Tsinakis},
pages = {99--103},
address = {Patras University, Greece},
publisher = {Patras University Press},
month = jul # { 15--19,},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/kuz09b.pdf},
year = 2009
}
@phdthesis{weh10,
author = {Wehbe, Ricardo},
title = {Annotated {S}ystems for {C}ommon {K}nowledge},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/weh10.pdf},
year = 2010
}
@phdthesis{sal05,
author = {Vincenzo Salipante},
title = {On the Consistency Strength of the Strict
${\Pi}^{1}_{1}$ Reflection Principle},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/sal05.pdf},
year = 2005
}
@article{JS11,
author = {J{\"a}ger, Gerhard and Studer, Thomas},
title = {A {B}uchholz rule for modal fixed point logics},
journal = {Logica Universalis},
volume = {5},
number = {1},
pages = {1--19},
doi = {10.1007/s11787-010-0022-1},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/js11.pdf},
year = 2011
}
@article{stu08,
author = {Thomas Studer},
title = {On the proof theory of the modal mu-calculus},
journal = {Studia Logica},
volume = {89},
number = {3},
pages = {343--363},
doi = {10.1007/s11225-008-9133-6},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/stu08.pdf},
year = 2008
}
@mastersthesis{ste01,
author = {David Steiner},
title = {Proof-Theoretic Strength of $\mathsf{PRON}$ with
Various Extensions},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/ste01.pdf},
year = 2001
}
@inproceedings{jae10,
author = {J{\"a}ger, Gerhard},
title = {Modal {F}ixed {P}oint {L}ogics},
booktitle = {Logics and {L}anguages for {R}eliability and
{S}ecurity},
editor = {{J. Esparza} and {B. Spanfelner} and {O. Grumberg}},
volume = {25},
series = {NATO Science for Peace and Security Series - D:
Information and Communication Security},
publisher = {IOS Press},
doi = {10.3233/978-1-60750-100-8-129},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/jae10.pdf},
year = 2010
}
@article{mck12a,
author = {Richard McKinley},
title = {Canonical proof nets for classical logic},
journal = {Annals of Pure and Applied Logic},
volume = 164,
number = 6,
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/mck12a.pdf},
year = 2013,
pages = {702-732},
issn = {0168-0072},
doi = {10.1016/j.apal.2012.05.007}
}
@article{mck12b,
author = {Richard McKinley},
title = {Proof Nets for {H}erbrand's {T}heorem},
journal = {ACM Transactions on Computational Logic},
volume = 14,
number = 1,
year = 2013,
pages = 5,
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/mck12b.pdf},
doi = {10.1145/2422085.2422090}
}
@incollection{alb02b,
author = {Luca Alberucci},
title = {Strictness of the modal $\mu$-calculus hierarchy},
booktitle = {Automata, Logics and infinite Games: A Guide to
Current Research},
publisher = {Springer},
editor = {Erich Gr{\"a}del and Wolfgang Thomas and Thomas Wilke},
volume = {2500},
series = {Lecture Notes in Computer Science},
pages = {185{--}201},
ps = {https://home.inf.unibe.ch/ltg/publications/2002/alb02b.ps},
year = 2002
}
@inproceedings{hjss95b,
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan
Schwendimann and Michael Seyfried},
title = {{LWB} - a logics workbench, extended abstract},
booktitle = {Proceedings of KI-95 Activities: Workshop, Posters,
Demos},
editor = {L. Dreschler-Fischer and S. Pribbenow},
pages = {73{--}74},
publisher = {Gesellschaft f{\"u}r Informatik},
year = 1995
}
@inproceedings{weh06a,
author = {Ricardo Wehbe},
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},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/weh06a.pdf},
year = 2006
}
@inproceedings{es12a,
author = {Eberhard, Sebastian and Strahm, Thomas},
title = {Weak theories of truth and explicit mathematics},
pages = {157{--}184},
editor = {Ulrich Berger and Hannes Diener and Peter Schuster
and Monika Seisenberger},
booktitle = {Logic, Construction, Computation},
year = 2012,
publisher = {Ontos Verlag},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/es12a.pdf}
}
@mastersthesis{buc99,
author = {Irene Bucher},
title = {Extension of the Modal System {KT4}},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
year = 1999
}
@incollection{str10,
author = {Strahm, Thomas},
title = {Weak theories of operations and types},
booktitle = {Ways of {P}roof {T}heory},
publisher = {Ontos Verlag},
editor = {{Ralf Schindler}},
pages = {441--468},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/str10.pdf},
year = 2010
}
@incollection{str99,
author = {Thomas Strahm},
title = {First steps into metapredicativity in explicit
mathematics},
booktitle = {Sets and Proofs},
publisher = {Cambridge University Press},
editor = {S. Barry Cooper and John K. Truss},
volume = {258},
series = {London Mathematical Society Lecture Notes},
pages = {383{--}402},
pdf = {https://home.inf.unibe.ch/ltg/publications/1999/str99.pdf},
year = 1999
}
@article{bks12a,
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
doi = {10.1016/j.jcss.2014.04.001},
journal = {Journal of Computer and System Sciences},
keywords = {Justification logic, Dynamic epistemic logic, Public
announcements, Belief revision},
number = {6},
pages = {1046--1066},
title = {{Realizing Public Announcements by Justifications}},
year = 2014,
volume = {80},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/bks12a.pdf},
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's belief. We present
${\sf OPAL(K)}$ and ${\sf JPAL(K)}$, two alternative
justification counterparts of
Gerbrandy--Groeneveld'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.}
}
@incollection{bks12b,
title = {{Decidability for Justification Logics Revisited}},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
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 = {justification logic, decidability, filtration},
booktitle = {Logic, Language, and Computation, 9th~International
{T}bilisi Symposium on Logic, Language, and
Computation, {TbiLLC~2011}, {K}utaisi, {G}eorgia,
{S}eptember 26-30, 2011, Revised Selected Papers},
doi = {10.1007/978-3-642-36976-6_12},
editor = {Guram Bezhanishvili and Sebastian L{\"o}bner and
Vincenzo Marra and Frank Richter},
pages = {166--181},
publisher = {Springer},
series = {LNCS},
volume = 7758,
year = 2013,
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/bks12b.pdf}
}
@incollection{ks13,
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.},
author = {Roman Kuznets and Thomas Studer},
booktitle = {Logical Foundations of Computer Science,
International Symposium, {LFCS}~2013, {S}an {D}iego,
{CA}, {USA}, {J}anuary 6--8, 2013, Proceedings},
doi = {10.1007/978-3-642-35722-0_19},
editor = {Sergei Artemov and Anil Nerode},
pages = {266--279},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {{Update as Evidence: Belief Expansion}},
volume = 7734,
year = 2013,
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/ks13.pdf}
}
@incollection{ks12,
author = {Roman Kuznets and Thomas Studer},
title = {{Justifications, Ontology, and Conservativity}},
editor = {Thomas Bolander and Torben Bra\"uner and Silvio
Ghilardi and Lawrence Moss},
booktitle = {Advances in Modal Logic, volume 9},
pages = {437--458},
publisher = {College Publications},
year = {2012},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/ks12.pdf}
}
@article{bs12,
author = {Br\"unnler, Kai and Studer, Thomas},
title = {Syntactic cut-elimination for a fragment of the
modal mu-calculus},
journal = {Annals of Pure and Applied Logic},
pages = {1838--1853},
volume = 163,
number = 12,
year = 2012,
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/bs12.pdf}
}
@article{stu12b,
author = {Studer, Thomas},
title = {{A Universal Approach to Guarantee Data Privacy}},
journal = {Logica Universalis},
year = 2013,
volume = 7,
number = 2,
pages = {195--209},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/stu12b.pdf}
}
@article{stu13,
author = {Studer, Thomas},
title = {Decidability for some justification logics with negative introspection},
journal = {The Journal of Symbolic Logic},
year = 2013,
volume = 78,
number = 2,
pages = {388--402},
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/stu13.pdf}
}
@techreport{bks10b,
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
title = {Explicit Evidence Systems with Common Knowledge},
institution = {arXiv.org},
type = {E-print},
number = {1005.0484},
abstract = {Justification logics are epistemic logics that
explicitly include justifications for the agents'
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'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'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.},
month = may,
url = {http://arxiv.org/abs/1005.0484},
year = 2010
}
@phdthesis{bal01,
author = {Peter Balsiger},
title = {The Mac{LWB} and the Logic of Likelihood},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/bal01.pdf},
year = 2001
}
@phdthesis{kre06,
author = {Mathis Kretz},
title = {Proof-Theoretic Aspects of Modal Logic with Fixed
Points},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/kre06.pdf},
year = 2006
}
@article{js01,
author = {Gerhard J{\"a}ger and Thomas Strahm},
title = {Upper bounds for metapredicative {M}ahlo in explicit
mathematics and admissible set theory},
journal = {The Journal of Symbolic Logic},
volume = {66},
number = {2},
pages = {935{--}958},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/js01.pdf},
year = 2001
}
@inproceedings{ks07,
author = {Norbert Kottmann and Thomas Studer},
title = {Improving semantic query answering},
booktitle = {Proceedings of Database and Expert Systems
Applications},
editor = {Roland Wagner and Norman Revell and G{\"u}nther Pernul},
volume = {4653},
series = {Lecture Notes in Computer Science},
pages = {671{--}679},
publisher = {Springer},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/ks07.pdf},
year = 2007
}
@inproceedings{ss09b,
author = {Stouppa, Phiniki and Studer, Thomas},
title = {Data {P}rivacy for {ALC} {K}nowledge {B}ases},
booktitle = {Proceedings of {L}ogical {F}oundations of {C}omputer
{S}cience {LFCS}'09},
editor = {{S. Artemov} and {A. Nerode}},
volume = {5407},
series = {LNCS},
pages = {409--421},
publisher = {Springer},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/ss09b.pdf},
year = 2009
}
@inproceedings{weh07b,
author = {Ricardo Wehbe},
title = {Merging rule-based belief databases},
booktitle = {Proceedings of Artificial Intelligence and
Applications},
editor = {Vladan Deved{\v{z}}i{\'c}},
pages = {585{--}589},
publisher = {ACTA Press},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/weh07b.pdf},
year = 2007
}
@mastersthesis{son05,
author = {Daniel Sonderegger},
title = {$\mathsf{PLTL}$ {--} {V}ollst{\"a}ndigkeit und
{M}odell-{K}onstruktion},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/son05.pdf},
year = 2005
}
@article{hjss96b,
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan
Schwendimann and Michael Seyfried},
title = {The logics workbench {LWB}: a snapshot},
journal = {Euromath Bulletin},
volume = {2},
number = {1},
pages = {177{--}186},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/hjss96b.ps},
year = 1996
}
@article{mck08,
author = {Richard McKinley},
title = {Soft linear set theory},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
number = {2},
pages = {226-245},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/mck08.pdf},
year = 2008
}
@article{jp11,
author = {Gerhard J{\"a}ger and Dieter Probst},
title = {The Suslin operator in applicative theories: Its
proof-theoretic analysis via ordinal theories},
journal = {Annals of Pure and Applied Logic},
volume = 162,
number = 8,
pages = {647--660},
doi = {10.1016/j.apal.2011.01.009},
issn = {0168-0072},
keywords = {Proof theory, Suslin operator in applicative theories,
Ordinal theories},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/jp11.pdf},
year = 2011
}
@article{ps01,
author = {Dieter Probst and Thomas Studer},
title = {How to normalize the {J}ay},
journal = {Theoretical Computer Science},
volume = {254},
number = {1{--}2},
pages = {677-681},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/ps01.pdf},
year = 2001
}
@article{jae04,
author = {Gerhard J{\"a}ger},
title = {An intensional fixed point theory over first order
arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {128},
number = {1{--}3},
pages = {197{--}213},
pdf = {https://home.inf.unibe.ch/ltg/publications/2004/jae04.pdf},
year = 2004
}
@article{jae09a,
author = {Gerhard J{\"a}ger},
title = {Full operational set theory with unbounded existential
quantification and power set},
journal = {Annals of Pure and Applied Logic},
volume = {160},
number = {1},
pages = {33--52},
month = jul,
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/jae09a.pdf},
year = 2009
}
@phdthesis{ste09,
author = {Steiner, David},
title = {Belief {C}hange {F}unctions for {M}ulti-{A}gent
{S}ystems},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/ste09.pdf},
year = 2009
}
@techreport{hs96b,
author = {Alain Heuerding and Stefan Schwendimann},
title = {A benchmark method for the propositional modal logics
{K}, {KT}, {S4}},
institution = {Universit{\"a}t Bern},
number = {IAM{--}96{--}015},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
ps = {https://home.inf.unibe.ch/ltg/publications/1996/hs96b.ps},
year = 1996
}
@inproceedings{ds05,
author = {Michael D{\"u}rig and Thomas Studer},
title = {Probabilistic {AB}ox reasoning: preliminary results},
booktitle = {Proceedings of Description Logics '05},
editor = {Ian Horrocks and Ulrike Sattler and Frank Wolter},
volume = {147},
series = {{CEUR} Workshop Proceedings},
pages = {104{--}111},
publisher = {CEUR-WS.org},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/ds05.pdf},
year = 2005
}
@mastersthesis{bru10a,
author = {Brugger, Jon},
title = {Proof-theoretic aspects of weak {K}\"onig's {L}emma},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/bru10a.pdf},
year = 2010
}
@inproceedings{bk09,
author = {Buss, Samuel R. and Kuznets, Roman},
title = {The {NP}-completeness of reflected fragments of
justification logics},
booktitle = {Proceedings of {S}ymposium on {L}ogical {F}oundations
of {C}omputer {S}cience ({LFCS}'09)},
editor = {Artemov, Sergei and Nerode, Anil},
volume = {5407},
series = {Lecture Notes in Computer Science},
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},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/bk09.pdf},
year = 2009
}
@article{bk12,
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.},
author = {Samuel R. Buss and Roman Kuznets},
doi = {10.1016/j.apal.2011.09.010},
journal = {Annals of Pure and Applied Logic},
keywords = {justification logic; logic of proofs; computational complexity; $\Pi^p_2$-completeness; Derivability problem},
month = jul,
note = {Published online November~2011},
number = {7},
pages = {888--905},
url = {http://www.sciencedirect.com/science/article/pii/S0168007211001321},
pdf = {http://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/APAL09_final.pdf},
title = {Lower complexity bounds in justification logic},
volume = {163},
year = {2012}
}
@techreport{stu10b,
author = {Thomas Studer},
title = {Proof-{T}heoretic {C}ontributions to {M}odal {F}ixed
{P}oint {L}ogics},
institution = {Universit{\"a}t Bern},
type = {Habilitationsschrift},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/stu10b.pdf},
year = 2010
}
@incollection{ow02,
author = {Geoffrey E. Ostrin and Stanley S. Wainer},
title = {Proof theoretic complexity},
booktitle = {Proof and System Reliability},
publisher = {Springer},
editor = {Helmut Schwichtenberg and Ralf Steinbr{\"u}ggen},
volume = {62},
series = {{NATO} Science Series},
pages = {369{--}398},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/ow02.pdf},
year = 2002
}
@article{str03,
author = {Thomas Strahm},
title = {Theories with self-application and computational
complexity},
journal = {Information and Computation},
volume = {185},
number = {2},
pages = {263{--}297},
pdf = {https://home.inf.unibe.ch/ltg/publications/2003/str03.pdf},
year = 2003
}
@incollection{jk10,
author = {J{\"a}ger, Gerhard and Kr{\"a}henb{\"u}hl, J{\"u}rg},
title = {${\Sigma^1_1}$ choice in a theory of sets and classes},
booktitle = {Ways of {P}roof {T}heory},
publisher = {Ontos Verlag},
editor = {{Ralf Schindler}},
pages = {283--314},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/jk10.pdf},
year = 2010
}
@mastersthesis{kra09,
author = {Kr{\"a}henb{\"u}hl, J{\"u}rg},
title = {Justifying induction on modal mu-formulae},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/kra09.pdf},
year = 2009
}
@article{str00b,
author = {Thomas Strahm},
title = {The non-constructive $\mu$-operator, fixed point
theories with ordinals, and the bar rule},
journal = {Annals of Pure and Applied Logic},
volume = {104},
number = {1{--}3},
pages = {305{--}324},
ps = {https://home.inf.unibe.ch/ltg/publications/2000/str00b.ps},
year = 2000
}
@article{str04,
author = {Thomas Strahm},
title = {A proof-theoretic characterization of the basic
feasible functionals},
journal = {Theoretical Computer Science},
volume = {329},
number = {1{--}3},
pages = {159{--}176},
pdf = {https://home.inf.unibe.ch/ltg/publications/2004/str04.pdf},
year = 2004
}
@article{ow05,
author = {Geoffrey E. Ostrin and Stanley S. Wainer},
title = {Elementary Arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {133},
number = {1{--}3},
pages = {275{--}292},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/ow05.pdf},
year = 2005
}
@inproceedings{ks00,
author = {Reinhard Kahle and Thomas Studer},
title = {A theory of explicit mathematics equivalent to
$\mathsf{ID}_{1}$},
booktitle = {Proceedings of Computer Science Logic},
editor = {Peter Clote and Helmut Schwichtenberg},
volume = {1862},
series = {Lecture Notes in Computer Science},
pages = {356{--}370},
publisher = {Springer},
pdf = {https://home.inf.unibe.ch/ltg/publications/2000/ks00.pdf},
year = 2000
}
@article{jp04b,
author = {Gerhard J{\"a}ger and Dieter Probst},
title = {Variation on a theme of {S}ch{\"u}tte},
journal = {Mathematical Logic Quarterly},
volume = {50},
number = {3},
pages = {258{--}264},
pdf = {https://home.inf.unibe.ch/ltg/publications/2004/jp04b.pdf},
year = 2004
}
@article{fj93,
author = {Solomon Feferman and Gerhard J{\"a}ger},
title = {Systems of explicit mathematics with non-constructive
$\mu$-operator. {P}art {I}},
journal = {Annals of Pure and Applied Logic},
volume = {65},
number = {3},
pages = {243{--}263},
pdf = {https://home.inf.unibe.ch/ltg/publications/1993/fj93.pdf},
year = 1993
}
@article{js93,
author = {Gerhard J{\"a}ger and Robert F. St{\"a}rk},
title = {The defining power of stratified and hierarchical
logic programs},
journal = {Journal of Logic Programming},
volume = {15},
number = {1{--}2},
pages = {55{--}77},
pdf = {https://home.inf.unibe.ch/ltg/publications/1993/js93.pdf},
year = 1993
}
@article{ss06,
author = {David Steiner and Thomas Strahm},
title = {On the proof theory of type two functionals based on
primitive recursive operations},
journal = {Mathematical Logic Quarterly},
volume = {52},
number = {3},
pages = {237{--}252},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/ss06.pdf},
year = 2006
}
@inproceedings{as93b,
author = {Sergei Artemov and Tyko Strassen},
title = {The Basic Logic of Proofs},
booktitle = {{C}omputer {S}cience {L}ogic, 6th Workshop, {CSL}'92,
{S}an {M}iniato, {I}taly, {S}eptember 28--{O}ctober 2,
1992, Selected Papers},
editor = {E. B{\"{o}}rger and G. J{\"{a}}ger and Kleine
B{\"{u}}ning, H. and S. Martini and M. M. Richter},
volume = 702,
series = {Lecture Notes in Computer Science},
pages = {14--28},
publisher = {Springer},
abstract = {Propositional Provability Logic was axiomatized
in~[Sol76]. This logic describes the behaviour of the
arithmetical operator ``$y$~is provable''. The aim of
the current paper is to provide propositional
axiomatizations of the predicate ``$x$~is a proof
of~$y$'' 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},
year = 1993,
zmath = {http://www.zentralblatt-math.org/zmath/en/search/?q=an:00515725&type=pdf&format=complete}
}
@article{aks14,
author = {Alberucci, Luca and Kr{\"a}henb{\"u}hl, J{\"u}rg and
Studer, Thomas},
title = {Justifying induction on modal $\mu$-formulae},
year = 2014,
volume = 22,
issue = 6,
pages = {805--817},
doi = {10.1093/jigpal/jzu001},
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$.},
pdf = {https://home.inf.unibe.ch/ltg/publications/2014/aks14.pdf},
eprint = {http://jigpal.oxfordjournals.org/content/early/2014/03/10/jigpal.jzu001.full.pdf+html},
journal = {Logic Journal of IGPL}
}
@article{stu01a,
author = {Thomas Studer},
title = {A semantics for $\lambda^{\{ \}}_{\mathsf{str}}$: a
calculus with overloading and late-binding},
journal = {Journal of Logic and Computation},
volume = {11},
number = {4},
pages = {527{--}544},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/stu01a.pdf},
year = 2001
}
@article{jkss99,
author = {Gerhard J{\"a}ger and Reinhard Kahle and Anton Setzer
and Thomas Strahm},
title = {The proof-theoretic analysis of transfinitely iterated
fixed point theories},
journal = {The Journal of Symbolic Logic},
volume = {64},
number = {1},
pages = {53{--}67},
pdf = {https://home.inf.unibe.ch/ltg/publications/1999/jkss99.ps},
year = 1999
}
@phdthesis{spe09,
author = {Spescha, Daria},
title = {Weak {S}ystems of {E}xplicit {M}athematics},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/spe09.pdf},
year = 2009
}
@phdthesis{kra11,
author = {Kr{\"a}henb{\"u}hl, J{\"u}rg},
title = {On the {R}elationship between {C}hoice {S}chemes and {I}terated {C}lass {C}omprehension in {S}et {T}heory},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/kra11.pdf},
year = 2011
}
@inproceedings{bejklm94,
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},
title = {Executable models for analysis and implementation of
complex systems},
booktitle = {Proceedings of Information Conference of Swiss
Priority Programme Informatics Research 1992{--}1996,
Module 1: Secure Distributed Systems},
year = 1994
}
@article{rs02,
author = {Christian R{\"u}ede and Thomas Strahm},
title = {Intuitionistic fixed point theories for strictly
positive operators},
journal = {Mathematical Logic Quarterly},
volume = {48},
number = {2},
pages = {195{--}202},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/rs02.pdf},
year = 2002
}
@inproceedings{bks11b,
author = {Bucheli, Samuel and Kuznets, Roman and Studer, Thomas},
title = {Partial {R}ealization in {D}ynamic {J}ustification
{L}ogic},
booktitle = {Logic, Language, Information and Computation, 18th
International Workshop, WoLLIC 2011, Philadelphia, PA,
USA, May 18-20, 2011, Proceedings},
volume = {6642},
pages = {35-51},
doi = {10.1007/978-3-642-20920-8_9},
editor = {Beklemishev, Lev D. and de Queiroz, Ruy},
series = {Lecture Notes in Artificial Intelligence},
pdf = {https://home.inf.unibe.ch/ltg/publications/2011/bks11b.pdf},
year = 2011
}
@article{js99,
author = {Gerhard J{\"a}ger and Thomas Strahm},
title = {Bar induction and $\omega$ model reflection},
journal = {Annals of Pure and Applied Logic},
volume = {97},
number = {1{--}3},
pages = {221{--}230},
pdf = {https://home.inf.unibe.ch/ltg/publications/1999/js99.ps},
year = 1999
}
@inproceedings{jae05,
author = {Gerhard J{\"a}ger},
title = {Metapredicative and explicit {M}ahlo: a
proof-theoretic perspective},
booktitle = {Proceedings of Logic Colloquium '00},
editor = {Rene Cori and Alexander Razborov and Stevo Todorcevic
and Carol Wood},
volume = {19},
series = {Association of Symbolic Logic Lecture Notes in Logic},
pages = {272{--}293},
publisher = {AK Peters},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/jae05.pdf},
year = 2005
}
@phdthesis{sch98b,
author = {Stefan Schwendimann},
title = {Aspects of Computational Logic},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/1998/sch98b.ps},
year = 1998
}
@article{stu09,
author = {Studer, Thomas},
title = {Common knowledge does not have the {B}eth property},
journal = {Information Processing Letters},
volume = {109},
pages = {611--614},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/stu09.pdf},
year = 2009
}
@article{jae93a,
author = {Gerhard J{\"a}ger},
title = {Fixed points in {P}eano arithmetic with ordinals},
journal = {Annals of Pure and Applied Logic},
volume = {60},
number = {2},
pages = {119{--}132},
doi = {10.1016/0168-0072(93)90039-G},
url = {http://dx.doi.org/10.1016/0168-0072(93)90039-G},
year = 1993
}
@inproceedings{jae09b,
author = {Gerhard J{\"a}ger},
title = {Operations, sets and classes},
booktitle = {Logic, {M}ethodology and {P}hilosophy of {S}cience -
{P}roceedings of the {T}hirteenth {I}nternational
{C}ongress},
editor = {{C. Glymour} and {W. Wei} and {D. Westerstahl}},
publisher = {College Publications},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/jae09b.pdf},
year = 2009
}
@mastersthesis{ebe09,
author = {Eberhard, Sebastian},
title = {Aspekte beweisbar totaler {F}unktionen in applikativen
{T}heorien},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2009/ebe09.pdf},
year = 2009
}
@article{ebe12a,
author = {Eberhard, Sebastian},
title = {A feasible theory of truth over combinatory algebra},
volume = 165,
number = 5,
pages = {1009--1033},
year = 2014,
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.12.002},
keywords = {Polytime computability},
keywords = {Applicative theories},
keywords = {Truth theories},
journal = {Annals of Pure and Applied Logic},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/ebe12a.pdf}
}
@phdthesis{ebe13,
author = {Eberhard, Sebastian},
title = {Weak applicative theories, truth, and computational
complexity},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/ebe13.pdf},
year = 2013
}
@phdthesis{bra13,
author = {Brambilla, Peppo},
title = {{Proof Search in Propositional Circumscription and Default Logic}},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/bra13.pdf},
year = 2013
}
@phdthesis{zum13,
author = {Zumbrunnen, Rico},
title = {{Contributions to Operational Set Theory}},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/zum13.pdf},
year = 2013
}
@phdthesis{flu13,
author = {Flumini, Dandolo},
title = {{Weak well orders}},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2013/flu13.pdf},
year = 2013
}
@mastersthesis{pul10,
author = {Pulver, Cornelia},
title = {Self-{R}eferentiality in {C}ontraction-free
{F}ragments of {M}odal {L}ogic {S}4},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/pul10.pdf},
year = 2010
}
@mastersthesis{koh12,
author = {Kohler, Roger Peter},
title = {Java-{P}rogramm zur interaktiven {B}earbeitung von {JALC}-{H}erleitungen},
type = {Bachelor's Thesis},
school = {Universit\"at Bern},
address = {Institut f\"ur Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/koh12.pdf},
year = 2012
}
@mastersthesis{lar08,
author = {Larrzabal, Ciro},
title = {Automatic {M}odel {C}hecking of {UML} models},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/lar08.pdf},
year = 2008
}
@incollection{sh98,
author = {Holger Schlingloff and Wolfgang Heinle},
title = {Relation Algebra and Modal Logics},
booktitle = {Relational Methods in Computer Science},
publisher = {Springer},
editor = {Chris Brink and Wolfram Kahl and Gunther Schmidt},
series = {Advances in Computer Science},
pages = {20{--}89},
year = 1998
}
@inproceedings{stu01b,
author = {Thomas Studer},
title = {Constructive foundations for {F}eatherweight {J}ava},
booktitle = {Proceedings of the International Seminar on Proof
Theory in Computer Science},
editor = {Reinhard Kahle and Peter Schroeder-Heister and Robert
F. St{\"a}rk},
volume = {2183},
series = {Lecture Notes in Computer Science},
pages = {202{--}238},
publisher = {Springer},
pdf = {https://home.inf.unibe.ch/ltg/publications/2001/stu01b.pdf},
year = 2001
}
@inproceedings{stu12,
author = {Thomas Studer},
title = {Justified Terminological Reasoning},
booktitle = {Proceedings of Perspectives of System Informatics PSI'11},
editor = {E. Clarke and I. Virbitskaite and A. Voronkov},
volume = {7162},
series = {Lecture Notes in Computer Science},
pages = {349{--}361},
publisher = {Springer},
pdf = {https://home.inf.unibe.ch/ltg/publications/2012/stu12.pdf},
year = 2012
}
@mastersthesis{stu97,
author = {Thomas Studer},
title = {Explicit Mathematics: W-type, Models},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
ps = {https://home.inf.unibe.ch/ltg/publications/1997/stu97.ps},
year = 1997
}
@mastersthesis{kot06,
author = {Norbert Kottmann},
title = {Description Logic Query Answering with Relational
Databases},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2006/kot06.pdf},
year = 2006
}
@article{as04,
author = {Luca Alberucci and Vincenzo Salipante},
title = {On modal $\mu$-calculus and non-well-founded set
theory},
journal = {Journal of Philosophical Logic},
volume = {33},
number = {4},
pages = {343{--}360},
pdf = {https://home.inf.unibe.ch/ltg/publications/2004/as04.pdf},
year = 2004
}
@article{str08b,
author = {Strahm, Thomas},
title = {Introduction},
journal = {Dialectica},
volume = {62},
number = {2},
pages = {145--147},
doi = {10.1111/j.1746-8361.2008.01143.x},
pdf = {https://home.inf.unibe.ch/ltg/publications/2008/str08b.pdf},
year = 2008
}
@inproceedings{bh98a,
author = {Peter Balsiger and Alain Heuerding},
title = {Comparison of Theorem Provers for Modal Logics {--}
Introduction and Summary},
booktitle = {Proceedings of Tableaux '98},
editor = {Harrie C. M. de Swart},
volume = {1397},
series = {Lecture Notes in Computer Science},
pages = {25{--}26},
publisher = {Springer},
year = 1998
}
@phdthesis{alb02a,
author = {Luca Alberucci},
title = {The Modal $\mu$-Calculus and the Logic of Common
Knowledge},
school = {Universit{\"a}t Bern},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/alb02a.pdf},
year = 2002
}
@inproceedings{tup00,
author = {Sergei Tupailo},
title = {Finitary reductions for local predicativity, {I}:
recursively regular ordinals},
booktitle = {Proceedings of Logic Colloquium '98},
editor = {Samuel S. Buss and Petr Hajek and Pavel Pudlak},
volume = {13},
series = {Association of Symbolic Logic Lecture Notes in Logic},
pages = {465{--}499},
publisher = {AK Peters},
year = 2000
}
@inproceedings{bl05,
author = {Kai Br{\"u}nnler and St{\'e}phane Lengrand},
title = {On two forms of bureaucracy in derivations},
booktitle = {Proceedings of Structures and Deduction},
editor = {Paola Bruscoli and Fran{\c{c}}ois Lamarche and Charles
Stewart},
pages = {65{--}74},
publisher = {Technische Universit{\"a}t Dresden},
pdf = {https://home.inf.unibe.ch/ltg/publications/2005/bl05.pdf},
year = 2005
}
@techreport{kah96b,
author = {Reinhard Kahle},
title = {{F}rege structures for partial applicative theories},
institution = {Universit{\"a}t Bern},
number = {IAM{--}96{--}013},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
year = 1996
}
@article{rue03a,
author = {Christian R{\"u}ede},
title = {The proof-theoretic analysis of ${\Sigma}^{1}_{1}$
transfinite dependent choice},
journal = {Annals of Pure and Applied Logic},
volume = {122},
number = {1{--}3},
pages = {195{--}234},
pdf = {https://home.inf.unibe.ch/ltg/publications/2003/rue03a.pdf},
year = 2003
}
@incollection{js02a,
author = {Gerhard J{\"a}ger and Thomas Strahm},
title = {The proof-theoretic analysis of the {S}uslin operator
in applicative theories},
booktitle = {Reflections on the Foundations of Mathematics: Essays
in Honor of Solomon Feferman},
publisher = {AK Peters},
editor = {Wilfried Sieg and Richard Sommer and Carolyn Talcott},
pages = {270{--}292},
pdf = {https://home.inf.unibe.ch/ltg/publications/2002/js02a.pdf},
year = 2002
}
@inproceedings{mck10a,
author = {Richard McKinley},
title = {Expansion nets: {P}roof nets for for propositional
classical logic},
booktitle = {Logic for Programming, Artificial Intelligence, and
Reasoning (LPAR 17)},
editor = {Fermüller, Christian and Voronkov, Andrei},
volume = {6397},
series = {Lecture Notes in Computer Science},
pages = {535-549},
publisher = {Springer Berlin / Heidelberg},
note = {10.1007/978-3-642-16242-8_38},
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/mck10a.pdf},
year = 2010
}
@article{jks07,
author = {Gerhard J{\"a}ger and Mathis Kretz and Thomas Studer},
title = {Cut-free common knowledge},
journal = {Journal of Applied Logic},
volume = {5},
number = {4},
pages = {681{--}689},
doi = {10.1016/j.jal.2006.02.003},
pdf = {https://home.inf.unibe.ch/ltg/publications/2007/jks07.pdf},
year = 2007
}
@inproceedings{bkrss10,
author = {Bucheli, Samuel and Kuznets, Roman and Renne, Bryan
and Sack, Joshua and Studer, Thomas},
title = {Justified {B}elief {C}hange},
booktitle = {Proceedings of the {S}econd {ILCLI} {I}nternational
{W}orkshop on {L}ogic and {P}hilosphy of {K}nowledge,
{C}ommunication and {A}ction ({L}og{KCA}-10)},
editor = {Arrazola, Xabier and Ponte, Mar\'{\i}a},
pages = {135--155},
publisher = {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--Groeneveld-style public
announcements.},
month = nov,
pdf = {https://home.inf.unibe.ch/ltg/publications/2010/bkrss10.pdf},
year = 2010
}
@techreport{wir99a,
author = {Marc Wirz},
title = {Characterizing the {G}rzegorczyk hierarchy by safe
recursion},
institution = {Universit{\"a}t Bern},
number = {IAM{--}99{--}005},
address = {Institut f{\"u}r Informatik und angewandte Mathematik},
pdf = {https://home.inf.unibe.ch/ltg/publications/1999/wir99a.pdf},
year = 1999
}
This file was generated by bibtex2html 1.99.