TY - JOUR
T1 - A flexible type system for the small Veblen ordinal
Y1 - Submitted
A1 - Ranzi, Florian
A1 - Thomas Strahm
UR - http://www.iam.unibe.ch/ltgpub/2016/rast16.pdf
ER -
TY - JOUR
T1 - From Mathesis Universalis to fixed points and related set-theoretic concepts
Y1 - Submitted
A1 - Gerhard Jäger
A1 - Silvia Steila
UR - http://www.iam.unibe.ch/ltgpub/2018/jast18.pdf
ER -
TY - JOUR
T1 - Some algebraic equivalent forms of R ⊆ L
JF - Fundamenta Mathematicae
Y1 - In Press
A1 - Silvia Steila
UR - http://www.iam.unibe.ch/ltgpub/2018/ste18.pdf
ER -
TY - JOUR
T1 - A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem
JF - The Journal of Symbolic Logic
Y1 - 2018
A1 - Paulo Oliva
A1 - Silvia Steila
UR - http://www.iam.unibe.ch/ltgpub/2017/os17.pdf
ER -
TY - JOUR
T1 - About some fixed point axioms and related principles in Kripke-Platek environments
JF - The Journal of Symbolic Logic
Y1 - 2018
A1 - Gerhard Jäger
A1 - Silvia Steila
AB - Starting point of this article are fixed point axioms for set-bounded monotone Σ_1 definable operators in the context of Kripke-Platek set theory KP. We analyze their relationship to other principles such as maximal iterations, bounded proper injections, and Σ_1 subset-bounded sparation. One of our main results states that in KP + (V =L) all these principles are equivalent to Σ_1 separation.
VL - 83
UR - http://www.iam.unibe.ch/ltgpub/2017/jast17.pdf
IS - 2
ER -
TY - JOUR
T1 - The strength of SCT soundness
JF - Journal of Logic and Computation
Y1 - 2018
A1 - Emanuele Frittaion
A1 - Pelupessy, Florian
A1 - Silvia Steila
A1 - Keita Yokoyama
ER -
TY - JOUR
T1 - Truncation and Semi-Decidability Notions in Applicative Theories
JF - The Journal of Symbolic Logic
Y1 - 2018
A1 - Gerhard Jäger
A1 - Timtej Rosebrock
A1 - Kentaro Sato
AB - BON+ is an applicative theory and closely related to the first order parts of the standard systems of explicit mathematics. As such it is also a natural framework for abstract computations. In this article we analyze this aspect of BON+ more closely. First a point is made for introducing a new operation τN , called truncation, to obtain a natural formalization of partial recursive functions in our applicative framework. Then we introduce the operational versions of a series of notions that are all equivalent to semi- decidability in ordinary recursion theory on the natural numbers, and study their mutual relationships over BON+ with τN .
VL - 83
UR - http://www.iam.unibe.ch/ltgpub/2016/jarosa16.pdf
IS - 03
ER -
TY - JOUR
T1 - Expressivity in Chain-Based Modal Logics
JF - Archive for Mathematical Logic
Y1 - 2017
A1 - Michel Marti
A1 - George Metcalfe
VL - 57
UR - http://www.iam.unibe.ch/ltgpub/2017/mame17.pdf
IS - 3–4
ER -
TY - JOUR
T1 - Generic Large Cardinals and Systems of Filters
JF - The Journal of Symbolic Logic
Y1 - 2017
A1 - Giorgio Audrito
A1 - Silvia Steila
VL - 82
UR - http://www.iam.unibe.ch/ltgpub/2017/as17.pdf
ER -
TY - JOUR
T1 - Logics with lower and upper probability operators
JF - International Journal of Approximate Reasoning
Y1 - 2017
A1 - Nenad Savić
A1 - Dragan Doder
A1 - Zoran Ognjanović
VL - 88
UR - http://www.iam.unibe.ch/ltgpub/2017/sdo17b.pdf
ER -
TY - JOUR
T1 - Ramsey's Theorem for Pairs and k Colors as a Sub-Classical Principle of Arithmetic
JF - Journal of Symbolic Logic
Y1 - 2017
A1 - Berardi, S.
A1 - Silvia Steila
VL - 82
UR - http://www.iam.unibe.ch/ltgpub/2016/best16.pdf
IS - 2
ER -
TY - JOUR
T1 - Intuitionistic common knowledge or belief
JF - Journal of Applied Logic
Y1 - 2016
A1 - Gerhard Jäger
A1 - Michel Marti
KW - Canonical models
KW - Common knowledge
KW - Intuitionistic modal logic
AB - 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 intuitionistic (common) knowledge/belief. Then we introduce corresponding deductive systems and show that they are sound and complete with respect to these semantics.
VL - 18
UR - http://www.iam.unibe.ch/ltgpub/2015/jmick15.pdf
ER -
TY - JOUR
T1 - Intuitionistic modal logic made explicit
JF - IfCoLog Journal of Logics and their Applications
Y1 - 2016
A1 - Michel Marti
A1 - Thomas Studer
VL - 3
UR - http://www.iam.unibe.ch/ltgpub/2016/mast16.pdf
IS - 5
ER -
TY - JOUR
T1 - Relativizing operational set theory
JF - The Bulletin of Symbolic Logic
Y1 - 2016
A1 - Gerhard Jäger
AB - We introduce a way of relativizing operational set theory that also takes care of application. After presenting the basic approach and proving some essential properties of this new form of relativization we turn to the notion of relativized regularity and to the system OST(LR) that extends OST by a limit axiom claiming that any set is element of a relativized regular set. Finally we show that OST(LR) is proof- theoretically equivalent to the well-known theory KPi for a recursively inaccessible universe.
VL - 22
UR - http://www.iam.unibe.ch/ltgpub/2015/jae15.pdf
ER -
TY - JOUR
T1 - Reverse mathematical bounds for the Termination Theorem
JF - Annals of Pure and Applied Logic
Y1 - 2016
A1 - Silvia Steila
A1 - Keita Yokoyama
AB - 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.
UR - http://www.iam.unibe.ch/ltgpub/2016/styo16.pdf
ER -
TY - JOUR
T1 - Weak arithmetical interpretations for the Logic of Proofs
JF - Logic Journal of IGPL
Y1 - 2016
A1 - Roman Kuznets
A1 - Thomas Studer
AB - 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.
VL - 24
UR - http://www.iam.unibe.ch/ltgpub/2016/kust16.pdf
ER -
TY - JOUR
T1 - A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP
JF - Annals of pure and applied logic
Y1 - 2015
A1 - Kentaro Sato
A1 - Rico Zumbrunnen
AB - We introduce a version of operational set theory, OST?, without a choice operation, which has a machinery for {$Δ$}0{$Δ$}0 separation based on truth functions and the separation operator, and a new kind of applicative set theory, so-called weak explicit set theory WEST, based on Gö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 à la Cohen and Krivine's classical realisability model.
PB - Elsevier
VL - 166
UR - http://www.iam.unibe.ch/ltgpub/2014/sz14.pdf
ER -
TY - JOUR
T1 - A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman's explicit mathematics T0
JF - Annals of pure and applied logic
Y1 - 2015
A1 - Kentaro Sato
AB - We partially solve a long-standing problem in the proof theory of explicit mathematics or the proof theory in general. Namely, we give a lower bound of Feferman?s system T0 of explicit mathematics (but only when formulated on classical logic) with a concrete interpretat ion of the subsystem {$Σ$}12-AC+ (BI) of second order arithmetic inside T0. Whereas a lower bound proof in the sense of proof-theoretic reducibility or of ordinalanalysis was already given in 80s, the lower bound in the sense of interpretability we give here is new. We apply the new interpretation method developed by the author and Zumbrunnen (2015), which can be seen as the third kind of model construction method for classical theories, after Cohen?s forcing and Krivine?s classical realizability. It gives us an interpretation between classical theories, by composing interpretations between intuitionistic theories.
PB - Elsevier
VL - 166
UR - http://www.iam.unibe.ch/ltgpub/2015/sat15b.pdf
ER -
TY - JOUR
T1 - Applicative theories for logarithmic complexity classes
JF - Theoretical Computer Science
Y1 - 2015
A1 - Sebastian Eberhard
AB - We present applicative theories of words corresponding to weak, and especially logarithmic, complexity classes. The theories for the logarithmic hierarchy and alternating logarithmic time formalise function algebras with concatenation recursion as main principle. We present two theories for logarithmic space where the first formalises a new two-sorted algebra which is very similar to Cook and Bellantoni's famous two-sorted algebra B for polynomial time [4]. The second theory describes logarithmic space by formalising concatenation- and sharply bounded recursion. All theories contain the predicates WW representing words, and VV representing temporary inaccessible words. They are inspired by Cantini's theories [6] formalising B.
PB - Elsevier
VL - 585
UR - http://www.iam.unibe.ch/ltgpub/2015/ebat15.pdf
ER -
TY - JOUR
T1 - First steps towards probabilistic justification logic
JF - Logic Journal of IGPL
Y1 - 2015
A1 - Ioannis Kokkinis
A1 - Petar Maksimović
A1 - Zoran Ognjanović
A1 - Thomas Studer
AB - 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.
PB - Oxford University Press
VL - 23
UR - http://www.iam.unibe.ch/ltgpub/2015/kmos15.pdf
ER -
TY - JOUR
T1 - Full and hat inductive definitions are equivalent in NBG
JF - Archive for Mathematical Logic
Y1 - 2015
A1 - Kentaro Sato
AB - 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ödel expansion of full n + 2-order number theory etc.) are. In this article, we establish the equivalence between {$Δ$}10{$\backslash$}bf-LFP and {$Δ$}10{$\backslash$}bf-FP, which assert the existence of a least and of a (not necessarily least) fixed point, respectively, for positive elementary operators (or between {$Δ$}n+20{$\backslash$}bf-LFP and {$Δ$}n+20{$\backslash$}bf-FP). Our proof also shows the equivalence between ID 1 and {\^{ }}ID1, both of which are defined in the standard way but with the starting theory PA replaced by ZFC (or full n + 2-th order number theory with global well-ordering).
PB - Springer
VL - 54
UR - http://www.iam.unibe.ch/ltgpub/2015/sat15a.pdf
ER -
TY - JOUR
T1 - Modal interpolation via nested sequents
JF - Annals of pure and applied logic
Y1 - 2015
A1 - Melvin Fitting
A1 - Roman Kuznets
AB - 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.
PB - Elsevier
VL - 166
UR - http://www.iam.unibe.ch/ltgpub/2015/fkm15.pdf
ER -
TY - JOUR
T1 - A feasible theory of truth over combinatory algebra
JF - Annals of Pure and Applied Logic
Y1 - 2014
A1 - Sebastian Eberhard
KW - Truth theories
VL - 165
UR - http://www.iam.unibe.ch/ltgpub/2012/ebe12a.pdf
ER -
TY - JOUR
T1 - A note on the theory $\mathsf{SID}_{{<}\omega}$ of stratified induction
JF - Mathematical Logic Quarterly
Y1 - 2014
A1 - Ranzi, Florian
A1 - Thomas Strahm
VL - 60
UR - http://www.iam.unibe.ch/ltgpub/2013/rs13.pdf
ER -
TY - JOUR
T1 - Censors for Boolean Description Logic
JF - Transactions on Data Privacy
Y1 - 2014
A1 - Thomas Studer
A1 - Johannes Werner
VL - 7
UR - http://www.iam.unibe.ch/ltgpub/2014/sw14.pdf
ER -
TY - JOUR
T1 - Explicit mathematics and operational set theory: some ontological comparisons
JF - The Bulletin of Symbolic Logic
Y1 - 2014
A1 - Gerhard Jäger
A1 - Rico Zumbrunnen
VL - 20
UR - http://www.iam.unibe.ch/ltgpub/2014/jz14.pdf
ER -
TY - JOUR
T1 - Forcing for Hat Inductive Definitions in Arithmetic – One of the Simplest Applications of Forcing –
JF - Mathematical Logic Quarterly
Y1 - 2014
A1 - Kentaro Sato
AB - 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''.
VL - 60
UR - http://www.iam.unibe.ch/ltgpub/2014/sat14.pdf
ER -
TY - JOUR
T1 - From hierarchies to well-foundedness
JF - Archive for Mathematical Logic
Y1 - 2014
A1 - Dandolo Flumini
A1 - Kentaro Sato
PB - Springer Berlin Heidelberg
VL - 53
UR - http://www.iam.unibe.ch/ltgpub/2014/fs14.pdf
ER -
TY - JOUR
T1 - Justifying induction on modal $μ$-formulae
JF - Logic Journal of IGPL
Y1 - 2014
A1 - Alberucci, Luca
A1 - Krähenbühl, Jürg
A1 - Thomas Studer
AB - 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$.
VL - 22
UR - http://www.iam.unibe.ch/ltgpub/2014/aks14.pdf
ER -
TY - JOUR
T1 - Logical Omniscience As Infeasibility
JF - Annals of Pure and Applied Logic
Y1 - 2014
A1 - Sergei Artemov
A1 - Roman Kuznets
AB - 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.
VL - 165
UR - http://www.iam.unibe.ch/ltgpub/2013/ak13.pdf
ER -
TY - JOUR
T1 - Proof Internalization for Generalized Frege Systems for Classical Logic
JF - Annals of Pure and Applied Logic
Y1 - 2014
A1 - Yury Savateev
AB - Abstract We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.
VL - 165
UR - http://www.iam.unibe.ch/ltgpub/2013/sav13a.pdf
ER -
TY - JOUR
T1 - Realizing Public Announcements by Justifications
JF - Journal of Computer and System Sciences
Y1 - 2014
A1 - Samuel Bucheli
A1 - Roman Kuznets
A1 - Thomas Studer
KW - Belief revision
KW - Dynamic epistemic logic
KW - justification logic
KW - Public announcements
AB - 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.
VL - 80
UR - http://www.iam.unibe.ch/ltgpub/2012/bks12a.pdf
ER -
TY - JOUR
T1 - Relative predicativity and dependent recursion in second-order set theory and higher-order theories
JF - The Journal of Symbolic Logic
Y1 - 2014
A1 - Kentaro Sato
VL - 79
UR - http://www.iam.unibe.ch/ltgpub/2012/sat12.pdf
ER -
TY - JOUR
T1 - A Universal Approach to Guarantee Data Privacy
JF - Logica Universalis
Y1 - 2013
A1 - Thomas Studer
VL - 7
UR - http://www.iam.unibe.ch/ltgpub/2012/stu12b.pdf
ER -
TY - JOUR
T1 - Canonical proof nets for classical logic
JF - Annals of Pure and Applied Logic
Y1 - 2013
A1 - Richard McKinley
VL - 164
UR - http://www.iam.unibe.ch/ltgpub/2012/mck12a.pdf
ER -
TY - JOUR
T1 - Decidability for some justification logics with negative introspection
JF - The Journal of Symbolic Logic
Y1 - 2013
A1 - Thomas Studer
VL - 78
UR - http://www.iam.unibe.ch/ltgpub/2013/stu13.pdf
ER -
TY - JOUR
T1 - Operational closure and stability
JF - Annals of Pure and Applied Logic
Y1 - 2013
A1 - Gerhard Jäger
AB - 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.
VL - 164
UR - http://www.iam.unibe.ch/ltgpub/2013/jae13.pdf
IS - 7-8
ER -
TY - JOUR
T1 - Proof Nets for Herbrand's Theorem
JF - ACM Transactions on Computational Logic
Y1 - 2013
A1 - Richard McKinley
VL - 14
UR - http://www.iam.unibe.ch/ltgpub/2012/mck12b.pdf
ER -
TY - JOUR
T1 - Lower complexity bounds in justification logic
JF - Annals of Pure and Applied Logic
Y1 - 2012
A1 - Buss, Samuel R.
A1 - Roman Kuznets
KW - Logic of Proofs
AB - 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.
VL - 163
UR - http://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/APAL09_final.pdf
N1 - Published online November 2011
ER -
TY - JOUR
T1 - Product-free Lambek calculus is NP-complete
JF - Annals of Pure and Applied Logic
Y1 - 2012
A1 - Yury Savateev
VL - 163
UR - http://www.iam.unibe.ch/ltgpub/2012/sav12.pdf
N1 - The Symposium on Logical Foundations of Computer Science 2009
ER -
TY - JOUR
T1 - Realization for Justification Logics via Nested Sequents: Modularity through Embedding
JF - Annals of Pure and Applied Logic
Y1 - 2012
A1 - Remo Goetschi
A1 - Roman Kuznets
VL - 163
UR - http://www.iam.unibe.ch/ltgpub/2012/gk12.pdf
ER -
TY - JOUR
T1 - Syntactic cut-elimination for a fragment of the modal mu-calculus
JF - Annals of Pure and Applied Logic
Y1 - 2012
A1 - Kai Brünnler
A1 - Thomas Studer
VL - 163
UR - http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf
ER -
TY - JOUR
T1 - A Buchholz rule for modal fixed point logics
JF - Logica Universalis
Y1 - 2011
A1 - Gerhard Jäger
A1 - Thomas Studer
VL - 5
UR - http://www.iam.unibe.ch/ltgpub/2011/js11.pdf
IS - 1
N1 - To appear, 2010
ER -
TY - JOUR
T1 - Admissible closures of polynomial time computable arithmetic
JF - Archive for Mathematical Logic
Y1 - 2011
A1 - Dieter Probst
A1 - Thomas Strahm
VL - 50
UR - http://www.iam.unibe.ch/ltgpub/2011/ps11.pdf
IS - 5-6
N1 - Submitted, 2010
ER -
TY - JOUR
T1 - Justification Logic, Inference Tracking, and Data Privacy
JF - Logic and Logical Philosophy
Y1 - 2011
A1 - Thomas Studer
VL - 20
UR - http://www.iam.unibe.ch/ltgpub/2011/stu11a.pdf
ER -
TY - JOUR
T1 - Justifications for Common Knowledge
JF - Journal of Applied Non-classical Logics
Y1 - 2011
A1 - Samuel Bucheli
A1 - Roman Kuznets
A1 - Thomas Studer
ED - Valentin Goranko
ED - Wojtek Jamroga
VL - 21
UR - http://www.iam.unibe.ch/ltgpub/2011/bks11a.pdf
IS - 1
N1 - To appear, 2011
ER -
TY - JOUR
T1 - Realizability in weak systems of explicit mathematics
JF - Mathematical Logic Quarterly
Y1 - 2011
A1 - Spescha, Daria
A1 - Thomas Strahm
VL - 57
UR - http://www.iam.unibe.ch/ltgpub/2011/ss11.pdf
IS - 6
N1 - To appear, 2010
ER -
TY - JOUR
T1 - The provably terminating operations of the subsystem PETJ of explicit mathematics
JF - Annals of Pure and Applied Logic
Y1 - 2011
A1 - Dieter Probst
VL - 162
UR - http://www.iam.unibe.ch/ltgpub/2011/pro11.pdf
IS - 11
N1 - Submitted, 2010
ER -
TY - JOUR
T1 - The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories
JF - Annals of Pure and Applied logic
Y1 - 2011
A1 - Gerhard Jäger
A1 - Dieter Probst
KW - Suslin operator in applicative theories
VL - 162
UR - http://www.iam.unibe.ch/ltgpub/2011/jp11.pdf
IS - 8
ER -
TY - JOUR
T1 - Self-Referential Justifications in Epistemic Logic
JF - Theory of Computing Systems
Y1 - 2010
A1 - Roman Kuznets
KW - self-referentiality
AB - 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.
VL - 46
UR - http://www.iam.unibe.ch/ltgpub/2010/kuz10.pdf
ER -
TY - JOUR
T1 - Unfolding finitist arithmetic
JF - Review of Symbolic Logic
Y1 - 2010
A1 - Solomon Feferman
A1 - Thomas Strahm
VL - 3
UR - http://www.iam.unibe.ch/ltgpub/2010/fs10.pdf
ER -
TY - JOUR
T1 - Common knowledge does not have the Beth property
JF - Information Processing Letters
Y1 - 2009
A1 - Thomas Studer
VL - 109
UR - http://www.iam.unibe.ch/ltgpub/2009/stu09.pdf
ER -
TY - JOUR
T1 - Deep Sequent Systems for Modal Logic
JF - Archive for Mathematical Logic
Y1 - 2009
A1 - Kai Brünnler
VL - 48
UR - http://www.iam.unibe.ch/ltgpub/2009/bru09.pdf
ER -
TY - JOUR
T1 - Elementary explicit types and polynomial time operations
JF - Mathematical Logic Quarterly
Y1 - 2009
A1 - Spescha, Daria
A1 - Thomas Strahm
VL - 55
UR - http://www.iam.unibe.ch/ltgpub/2009/ss09a.pdf
ER -
TY - JOUR
T1 - Full operational set theory with unbounded existential quantification and power set
JF - Annals of Pure and Applied Logic
Y1 - 2009
A1 - Gerhard Jäger
VL - 160
UR - http://www.iam.unibe.ch/ltgpub/2009/jae09a.pdf
ER -
TY - JOUR
T1 - On modal $μ$-calculus and Gödel-Löb logic
JF - Studia Logica
Y1 - 2009
A1 - Luca Alberucci
A1 - Alessandro Facchini
VL - 91
UR - http://www.iam.unibe.ch/ltgpub/2009/af09a.pdf
ER -
TY - JOUR
T1 - Sequent calculi for the modal $μ$-calculus over $\mathsf {S5}$
JF - Journal of Logic and Computation
Y1 - 2009
A1 - Luca Alberucci
UR - http://www.iam.unibe.ch/ltgpub/2009/alb09.pdf
N1 - Published online on January 22, 2009
ER -
TY - JOUR
T1 - Syntactic cut-elimination for common knowledge
JF - Annals of Pure and Applied Logic
Y1 - 2009
A1 - Kai Brünnler
A1 - Thomas Studer
VL - 160
UR - http://www.iam.unibe.ch/ltgpub/2009/bs09b.pdf
ER -
TY - JOUR
T1 - The modal $μ$-calculus hierarchy over restricted classes of transition systems
JF - Journal of Symbolic Logic
Y1 - 2009
A1 - Luca Alberucci
A1 - Alessandro Facchini
VL - 74
UR - http://www.iam.unibe.ch/ltgpub/2009/af09b.pdf
ER -
TY - JOUR
T1 - Canonical completeness of infinitary mu
JF - Journal of Logic and Algebraic Programming
Y1 - 2008
A1 - Gerhard Jäger
A1 - Mathis Kretz
A1 - Thomas Studer
VL - 76
UR - http://www.iam.unibe.ch/ltgpub/2008/jks08.pdf
ER -
TY - JOUR
T1 - Cut-free sequent systems for temporal logic
JF - Journal of Logic and Algebraic Programming
Y1 - 2008
A1 - Kai Brünnler
A1 - Lange, Martin
VL - 76
UR - http://www.iam.unibe.ch/ltgpub/2008/bl08.pdf
ER -
TY - JOUR
T1 - Introduction
JF - Dialectica
Y1 - 2008
A1 - Thomas Strahm
VL - 62
UR - http://www.iam.unibe.ch/ltgpub/2008/str08b.pdf
ER -
TY - JOUR
T1 - On contraction and the modal fragment
JF - Mathematical Logic Quarterly
Y1 - 2008
A1 - Kai Brünnler
A1 - Dieter Probst
A1 - Thomas Studer
VL - 54
UR - http://www.iam.unibe.ch/ltgpub/2008/bps08.pdf
ER -
TY - JOUR
T1 - On the proof theory of the modal mu-calculus
JF - Studia Logica
Y1 - 2008
A1 - Thomas Studer
VL - 89
UR - http://www.iam.unibe.ch/ltgpub/2008/stu08.pdf
ER -
TY - JOUR
T1 - Primitive recursive selection functions for existential assertions over abstract algebras
JF - Journal of Logic and Algebraic Programming
Y1 - 2008
A1 - Thomas Strahm
A1 - Zucker, Jeffery I
VL - 76
UR - http://www.iam.unibe.ch/ltgpub/2008/sz08.pdf
ER -
TY - JOUR
T1 - Soft linear set theory
JF - Journal of Logic and Algebraic Programming
Y1 - 2008
A1 - Richard McKinley
VL - 76
UR - http://www.iam.unibe.ch/ltgpub/2008/mck08.pdf
ER -
TY - JOUR
T1 - A deep inference system for the modal logic $\mathsf S5$
JF - Studia Logica
Y1 - 2007
A1 - Phiniki Stouppa
VL - 85
UR - http://www.iam.unibe.ch/ltgpub/2007/sto07.pdf
ER -
TY - JOUR
T1 - Cut-free common knowledge
JF - Journal of Applied Logic
Y1 - 2007
A1 - Gerhard Jäger
A1 - Mathis Kretz
A1 - Thomas Studer
VL - 5
UR - http://www.iam.unibe.ch/ltgpub/2007/jks07.pdf
ER -
TY - JOUR
T1 - On Feferman's operational set theory $\mathsf{OST}$
JF - Annals of Pure and Applied Logic
Y1 - 2007
A1 - Gerhard Jäger
VL - 150
UR - http://www.iam.unibe.ch/ltgpub/2007/jae07.pdf
ER -
TY - JOUR
T1 - Cut elimination inside a deep inference system for classical predicate logic
JF - Studia Logica
Y1 - 2006
A1 - Kai Brünnler
VL - 82
UR - http://www.iam.unibe.ch/ltgpub/2006/bru06a.pdf
ER -
TY - JOUR
T1 - Deduction chains for common knowledge
JF - Journal of Applied Logic
Y1 - 2006
A1 - Mathis Kretz
A1 - Thomas Studer
VL - 4
UR - http://www.iam.unibe.ch/ltgpub/2006/ks06.pdf
ER -
TY - JOUR
T1 - Locality for classical logic
JF - Notre Dame Journal of Formal Logic
Y1 - 2006
A1 - Kai Brünnler
VL - 47
UR - http://www.iam.unibe.ch/ltgpub/2006/bru06d.pdf
ER -
TY - JOUR
T1 - On the proof theory of type two functionals based on primitive recursive operations
JF - Mathematical Logic Quarterly
Y1 - 2006
A1 - David Steiner
A1 - Thomas Strahm
VL - 52
UR - http://www.iam.unibe.ch/ltgpub/2006/ss06.pdf
ER -
TY - JOUR
T1 - The proof-theoretic analysis of transfinitely iterated quasi least fixed points
JF - The Journal of Symbolic Logic
Y1 - 2006
A1 - Dieter Probst
VL - 71
UR - http://www.iam.unibe.ch/ltgpub/2006/pro06.pdf
ER -
TY - JOUR
T1 - About cut elimination for logics of common knowledge
JF - Annals of Pure and Applied Logic
Y1 - 2005
A1 - Luca Alberucci
A1 - Gerhard Jäger
VL - 133
UR - http://www.iam.unibe.ch/ltgpub/2005/aj05.pdf
ER -
TY - JOUR
T1 - Elementary Arithmetic
JF - Annals of Pure and Applied Logic
Y1 - 2005
A1 - Geoffrey E. Ostrin
A1 - Stanley S. Wainer
VL - 133
UR - http://www.iam.unibe.ch/ltgpub/2005/ow05.pdf
ER -
TY - JOUR
T1 - Explicit mathematics: power types and overloading
JF - Annals of Pure and Applied Logic
Y1 - 2005
A1 - Thomas Studer
VL - 134
UR - http://www.iam.unibe.ch/ltgpub/2005/stu05a.pdf
ER -
TY - JOUR
T1 - On the relationship between fixed points and iteration in admissible set theory without foundation
JF - Archive for Mathematical Logic
Y1 - 2005
A1 - Dieter Probst
VL - 44
UR - http://www.iam.unibe.ch/ltgpub/2005/pro05a.pdf
ER -
TY - JOUR
T1 - Reflections on reflections in explicit mathematics
JF - Annals of Pure and Applied Logic
Y1 - 2005
A1 - Gerhard Jäger
A1 - Thomas Strahm
VL - 136
UR - http://www.iam.unibe.ch/ltgpub/2005/js05.pdf
ER -
TY - JOUR
T1 - A proof-theoretic characterization of the basic feasible functionals
JF - Theoretical Computer Science
Y1 - 2004
A1 - Thomas Strahm
VL - 329
UR - http://www.iam.unibe.ch/ltgpub/2004/str04.pdf
ER -
TY - JOUR
T1 - An intensional fixed point theory over first order arithmetic
JF - Annals of Pure and Applied Logic
Y1 - 2004
A1 - Gerhard Jäger
VL - 128
UR - http://www.iam.unibe.ch/ltgpub/2004/jae04.pdf
ER -
TY - JOUR
T1 - On modal $μ$-calculus and non-well-founded set theory
JF - Journal of Philosophical Logic
Y1 - 2004
A1 - Luca Alberucci
A1 - Vincenzo Salipante
VL - 33
UR - http://www.iam.unibe.ch/ltgpub/2004/as04.pdf
ER -
TY - JOUR
T1 - Variation on a theme of Schütte
JF - Mathematical Logic Quarterly
Y1 - 2004
A1 - Gerhard Jäger
A1 - Dieter Probst
VL - 50
UR - http://www.iam.unibe.ch/ltgpub/2004/jp04b.pdf
ER -
TY - JOUR
T1 - Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe
JF - Annals of Pure and Applied Logic
Y1 - 2003
A1 - Sergei Tupailo
VL - 120
UR - http://www.iam.unibe.ch/ltgpub/2003/tup03.ps
ER -
TY - JOUR
T1 - The proof-theoretic analysis of $Σ^1_1$ transfinite dependent choice
JF - Annals of Pure and Applied Logic
Y1 - 2003
A1 - Christian Rüede
VL - 122
UR - http://www.iam.unibe.ch/ltgpub/2003/rue03a.pdf
ER -
TY - JOUR
T1 - Theories with self-application and computational complexity
JF - Information and Computation
Y1 - 2003
A1 - Thomas Strahm
VL - 185
UR - http://www.iam.unibe.ch/ltgpub/2003/str03.pdf
ER -
TY - JOUR
T1 - Universes in metapredicative analysis
JF - Archive for Mathematical Logic
Y1 - 2003
A1 - Christian Rüede
VL - 42
UR - http://www.iam.unibe.ch/ltgpub/2003/rue03b.pdf
ER -
TY - JOUR
T1 - Extending the system $\mathsf{T}_0$ of explicit mathematics: the limit and Mahlo axioms
JF - Annals of Pure and Applied Logic
Y1 - 2002
A1 - Gerhard Jäger
A1 - Thomas Studer
VL - 114
UR - http://www.iam.unibe.ch/ltgpub/2002/js02b.pdf
ER -
TY - JOUR
T1 - Intuitionistic fixed point theories for strictly positive operators
JF - Mathematical Logic Quarterly
Y1 - 2002
A1 - Christian Rüede
A1 - Thomas Strahm
VL - 48
UR - http://www.iam.unibe.ch/ltgpub/2002/rs02.pdf
ER -
TY - JOUR
T1 - Transfinite dependent choice and $\omega$-model reflection
JF - The Journal of Symbolic Logic
Y1 - 2002
A1 - Christian Rüede
VL - 67
UR - http://www.iam.unibe.ch/ltgpub/2002/rue02.pdf
ER -
TY - JOUR
T1 - Wellordering proofs for metapredicative Mahlo
JF - The Journal of Symbolic Logic
Y1 - 2002
A1 - Thomas Strahm
VL - 67
UR - http://www.iam.unibe.ch/ltgpub/2002/str02.pdf
ER -
TY - JOUR
T1 - A semantics for $\lambda^{\{\}}_{\mathsf str}$: a calculus with overloading and late-binding
JF - Journal of Logic and Computation
Y1 - 2001
A1 - Thomas Studer
VL - 11
UR - http://www.iam.unibe.ch/ltgpub/2001/stu01a.pdf
ER -
TY - JOUR
T1 - First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo
JF - The Journal of Symbolic Logic
Y1 - 2001
A1 - Gerhard Jäger
VL - 66
UR - http://www.iam.unibe.ch/ltgpub/2001/jae01.pdf
ER -
TY - JOUR
T1 - Formalizing non-termination of recursive programs
JF - Journal of Logic and Algebraic Programming
Y1 - 2001
A1 - Reinhard Kahle
A1 - Thomas Studer
VL - 49
UR - http://www.iam.unibe.ch/ltgpub/2001/ks01.pdf
ER -
TY - JOUR
T1 - How to normalize the Jay
JF - Theoretical Computer Science
Y1 - 2001
A1 - Dieter Probst
A1 - Thomas Studer
VL - 254
UR - http://www.iam.unibe.ch/ltgpub/2001/ps01.pdf
ER -
TY - JOUR
T1 - Realization of analysis into explicit mathematics
JF - The Journal of Symbolic Logic
Y1 - 2001
A1 - Sergei Tupailo
VL - 66
UR - http://www.iam.unibe.ch/ltgpub/2001/tup01.pdf
ER -
TY - JOUR
T1 - Universes in explicit mathematics
JF - Annals of Pure and Applied Logic
Y1 - 2001
A1 - Gerhard Jäger
A1 - Reinhard Kahle
A1 - Thomas Studer
VL - 109
UR - http://www.iam.unibe.ch/ltgpub/2001/jks01.pdf
ER -
TY - JOUR
T1 - Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory
JF - The Journal of Symbolic Logic
Y1 - 2001
A1 - Gerhard Jäger
A1 - Thomas Strahm
VL - 66
UR - http://www.iam.unibe.ch/ltgpub/2001/js01.pdf
ER -
TY - JOUR
T1 - A benchmark method for the propositional modal logics K, KT, S4
JF - Journal of Automated Reasoning
Y1 - 2000
A1 - Peter Balsiger
A1 - Alain Heuerding
A1 - Stefan Schwendimann
VL - 24
UR - http://www.iam.unibe.ch/ltgpub/2000/bhs00.pdf
ER -
TY - JOUR
T1 - Fixed point theories and dependent choice
JF - Archive for Mathematical Logic
Y1 - 2000
A1 - Gerhard Jäger
A1 - Thomas Strahm
VL - 39
UR - http://www.iam.unibe.ch/ltgpub/2000/js00.ps
ER -
TY - JOUR
T1 - N-strictness in applicative theories
JF - Archive for Mathematical Logic
Y1 - 2000
A1 - Reinhard Kahle
VL - 39
UR - http://dx.doi.org/10.1007/s001530050007
ER -
TY - JOUR
T1 - The non-constructive $μ$-operator, fixed point theories with ordinals, and the bar rule
JF - Annals of Pure and Applied Logic
Y1 - 2000
A1 - Thomas Strahm
VL - 104
UR - http://www.iam.unibe.ch/ltgpub/2000/str00b.ps
ER -
TY - JOUR
T1 - The unfolding of non-finitist arithmetic
JF - Annals of Pure and Applied Logic
Y1 - 2000
A1 - Solomon Feferman
A1 - Thomas Strahm
VL - 104
UR - http://www.iam.unibe.ch/ltgpub/2000/fs00.ps
ER -
TY - JOUR
T1 - Bar induction and $\omega$ model reflection
JF - Annals of Pure and Applied Logic
Y1 - 1999
A1 - Gerhard Jäger
A1 - Thomas Strahm
VL - 97
UR - http://www.iam.unibe.ch/ltgpub/1999/js99.ps
ER -
TY - JOUR
T1 - The proof-theoretic analysis of transfinitely iterated fixed point theories
JF - The Journal of Symbolic Logic
Y1 - 1999
A1 - Gerhard Jäger
A1 - Reinhard Kahle
A1 - Anton Setzer
A1 - Thomas Strahm
VL - 64
UR - http://www.iam.unibe.ch/ltgpub/1999/jkss99.ps
ER -
TY - JOUR
T1 - Frege structures for partial applicative theories
JF - Journal of Logic and Computation
Y1 - 1998
A1 - Reinhard Kahle
VL - 8
UR - http://dx.doi.org/10.1093/logcom/9.5.683
ER -
TY - JOUR
T1 - The $μ$ quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals
JF - Archive for Mathematical Logic
Y1 - 1998
A1 - Markus Marzetta
A1 - Thomas Strahm
VL - 37
UR - http://www.iam.unibe.ch/ltgpub/1998/ms98.ps
ER -
TY - JOUR
T1 - Polynomial time operations in explicit mathematics
JF - The Journal of Symbolic Logic
Y1 - 1997
A1 - Thomas Strahm
VL - 62
UR - http://www.iam.unibe.ch/ltgpub/1997/str97.ps
ER -
TY - JOUR
T1 - Power types in explicit mathematics?
JF - The Journal of Symbolic Logic
Y1 - 1997
A1 - Gerhard Jäger
VL - 62
UR - http://www.jstor.org/stable/2275630
ER -
TY - JOUR
T1 - Relations between propositional normal modal logics: an overview
JF - Journal of Logic and Computation
Y1 - 1997
A1 - Rajeev Goré
A1 - Wolfgang Heinle
A1 - Alain Heuerding
VL - 7
UR - http://www.iam.unibe.ch/ltgpub/1997/ghh97.ps
ER -
TY - JOUR
T1 - A logics workbench
JF - The European Journal on Artificial Intelligence
Y1 - 1996
A1 - Alain Heuerding
A1 - Gerhard Jäger
A1 - Stefan Schwendimann
A1 - Michael Seyfried
VL - 9
ER -
TY - JOUR
T1 - LWBtheory: information about some propositional logics via the WWW
JF - Journal of the Interest Group in Pure and Applied Logic
Y1 - 1996
A1 - Alain Heuerding
VL - 4
UR - http://www.iam.unibe.ch/ltgpub/1996/heu96.ps
ER -
TY - JOUR
T1 - Partial applicative theories and explicit substitutions
JF - Journal of Logic and Computation
Y1 - 1996
A1 - Thomas Strahm
VL - 6
UR - http://www.iam.unibe.ch/ltgpub/1996/str96b.ps
ER -
TY - JOUR
T1 - Some theories with positive induction of ordinal strength $\varphi \omega 0$
JF - The Journal of Symbolic Logic
Y1 - 1996
A1 - Gerhard Jäger
A1 - Thomas Strahm
VL - 61
UR - http://www.iam.unibe.ch/ltgpub/1996/js96.ps
ER -
TY - JOUR
T1 - Systems of explicit mathematics with non-constructive $μ$-operator and join
JF - Annals of Pure and Applied Logic
Y1 - 1996
A1 - Thomas Glass
A1 - Thomas Strahm
VL - 82
UR - http://www.iam.unibe.ch/ltgpub/1996/gs96.ps
ER -
TY - JOUR
T1 - Systems of explicit mathematics with non-constructive $μ$-operator. Part II
JF - Annals of Pure and Applied Logic
Y1 - 1996
A1 - Solomon Feferman
A1 - Gerhard Jäger
VL - 79
UR - http://dx.doi.org/10.1016/0168-0072(95)00028-3
ER -
TY - JOUR
T1 - The logics workbench LWB: a snapshot
JF - Euromath Bulletin
Y1 - 1996
A1 - Alain Heuerding
A1 - Gerhard Jäger
A1 - Stefan Schwendimann
A1 - Michael Seyfried
VL - 2
UR - http://www.iam.unibe.ch/ltgpub/1996/hjss96b.ps
ER -
TY - JOUR
T1 - Second order theories with ordinals and elementary comprehension
JF - Archive for Mathematical Logic
Y1 - 1995
A1 - Gerhard Jäger
A1 - Thomas Strahm
VL - 34
UR - http://www.iam.unibe.ch/ltgpub/1995/js95a.ps
ER -
TY - JOUR
T1 - Totality in applicative theories
JF - Annals of Pure and Applied Logic
Y1 - 1995
A1 - Gerhard Jäger
A1 - Thomas Strahm
VL - 74
UR - http://www.iam.unibe.ch/ltgpub/1995/js95b.ps
ER -
TY - JOUR
T1 - About some symmetries of negation
JF - The Journal of Symbolic Logic
Y1 - 1994
A1 - Brigitte Hösli
A1 - Gerhard Jäger
VL - 59
UR - http://www.jstor.org/stable/2275401
ER -
TY - JOUR
T1 - Fixed points in Peano arithmetic with ordinals
JF - Annals of Pure and Applied Logic
Y1 - 1993
A1 - Gerhard Jäger
VL - 60
UR - http://dx.doi.org/10.1016/0168-0072(93)90039-G
ER -
TY - JOUR
T1 - Systems of explicit mathematics with non-constructive $μ$-operator. Part I
JF - Annals of Pure and Applied Logic
Y1 - 1993
A1 - Solomon Feferman
A1 - Gerhard Jäger
VL - 65
UR - http://www.iam.unibe.ch/ltgpub/1993/fj93.pdf
ER -
TY - JOUR
T1 - The defining power of stratified and hierarchical logic programs
JF - Journal of Logic Programming
Y1 - 1993
A1 - Gerhard Jäger
A1 - Robert F. Stärk
VL - 15
UR - http://www.iam.unibe.ch/ltgpub/1993/js93.pdf
ER -