@article {1780,
title = {A flexible type system for the small Veblen ordinal},
year = {Submitted},
url = {http://www.iam.unibe.ch/ltgpub/2016/rast16.pdf},
author = {Ranzi, Florian and Thomas Strahm}
}
@article {1902,
title = {From Mathesis Universalis to fixed points and related set-theoretic concepts},
year = {Submitted},
url = {http://www.iam.unibe.ch/ltgpub/2018/jast18.pdf},
author = {Gerhard J{\"a}ger and Silvia Steila}
}
@article {1921,
title = {Some algebraic equivalent forms of R ⊆ L},
journal = {Fundamenta Mathematicae},
year = {In Press},
url = {http://www.iam.unibe.ch/ltgpub/2018/ste18.pdf},
author = {Silvia Steila}
}
@article {1896,
title = {A Direct Proof of Schwichtenberg{\textquoteright}s Bar Recursion Closure Theorem},
journal = {The Journal of Symbolic Logic},
year = {2018},
pages = {1-14},
doi = {10.1017/jsl.2017.33},
url = {http://www.iam.unibe.ch/ltgpub/2017/os17.pdf},
author = {Paulo Oliva and Silvia Steila}
}
@article {1833,
title = {About some fixed point axioms and related principles in Kripke-Platek environments},
journal = {The Journal of Symbolic Logic},
volume = {83},
year = {2018},
pages = {642-668},
abstract = {Starting point of this article are fixed point axioms for set-bounded
monotone Σ_1 definable operators in the context of Kripke-Platek set
theory KP. We analyze their relationship to other principles such as
maximal iterations, bounded proper injections, and Σ_1 subset-bounded
sparation. One of our main results states that in KP + (V =L) all these
principles are equivalent to Σ_1 separation.},
url = {http://www.iam.unibe.ch/ltgpub/2017/jast17.pdf},
author = {Gerhard J{\"a}ger and Silvia Steila}
}
@article {1894,
title = {The strength of SCT soundness},
journal = {Journal of Logic and Computation},
year = {2018},
doi = {10.1093/logcom/exy003},
author = {Emanuele Frittaion and Pelupessy, Florian and Silvia Steila and Keita Yokoyama}
}
@article {1812,
title = {Truncation and Semi-Decidability Notions in Applicative Theories},
journal = {The Journal of Symbolic Logic},
volume = {83},
year = {2018},
pages = {967-990},
abstract = {BON+ is an applicative theory and closely related to the first order parts of
the standard systems of explicit mathematics. As such it is also a natural framework
for abstract computations. In this article we analyze this aspect of BON+ more closely.
First a point is made for introducing a new operation τN , called truncation, to obtain a
natural formalization of partial recursive functions in our applicative framework. Then we
introduce the operational versions of a series of notions that are all equivalent to semi-
decidability in ordinary recursion theory on the natural numbers, and study their mutual
relationships over BON+ with τN .},
doi = {10.7892/boris.125568},
url = {http://www.iam.unibe.ch/ltgpub/2016/jarosa16.pdf},
author = {Gerhard J{\"a}ger and Timtej Rosebrock and Kentaro Sato}
}
@article {marti-metcalfe16,
title = {Expressivity in Chain-Based Modal Logics},
journal = {Archive for Mathematical Logic},
volume = {57},
year = {2017},
pages = {361-380},
url = {http://www.iam.unibe.ch/ltgpub/2017/mame17.pdf},
author = {Michel Marti and George Metcalfe}
}
@article {1895,
title = {Generic Large Cardinals and Systems of Filters},
journal = {The Journal of Symbolic Logic},
volume = {82},
year = {2017},
pages = {860-892},
doi = {10.1017/jsl.2017.27},
url = {http://www.iam.unibe.ch/ltgpub/2017/as17.pdf},
author = {Giorgio Audrito and Silvia Steila}
}
@article {1853,
title = {Logics with lower and upper probability operators},
journal = {International Journal of Approximate Reasoning},
volume = {88},
year = {2017},
pages = {148-168},
issn = {0888-613X},
url = {http://www.iam.unibe.ch/ltgpub/2017/sdo17b.pdf},
author = {Nenad Savi{\'c} and Dragan Doder and Zoran Ognjanovi{\'c}}
}
@article {ste16,
title = {Ramsey{\textquoteright}s Theorem for Pairs and k Colors as a Sub-Classical Principle of Arithmetic},
journal = {Journal of Symbolic Logic},
volume = {82},
year = {2017},
pages = {737-753},
url = {http://www.iam.unibe.ch/ltgpub/2016/best16.pdf},
author = {Berardi, S. and Silvia Steila}
}
@article {1731,
title = {Intuitionistic common knowledge or belief},
journal = {Journal of Applied Logic},
volume = {18},
year = {2016},
chapter = {150},
abstract = {Starting off from the usual language of modal logic for multi-agent systems dealing with the agents{\textquoteright} knowledge/belief and common knowledge/belief we define so-called epistemic Kripke structures for intuitionistic (common) knowledge/belief. Then we introduce corresponding deductive systems and show that they are sound and complete with respect to these semantics.},
keywords = {Canonical models, Common knowledge, Intuitionistic modal logic},
doi = {10.7892/boris.71315},
url = {http://www.iam.unibe.ch/ltgpub/2015/jmick15.pdf},
author = {Gerhard J{\"a}ger and Michel Marti}
}
@article {1783,
title = {Intuitionistic modal logic made explicit},
journal = {IfCoLog Journal of Logics and their Applications},
volume = {3},
year = {2016},
pages = {877-901},
url = {http://www.iam.unibe.ch/ltgpub/2016/mast16.pdf},
author = {Michel Marti and Thomas Studer}
}
@article {1753,
title = {Relativizing operational set theory},
journal = {The Bulletin of Symbolic Logic},
volume = {22},
year = {2016},
month = {09},
pages = {332-352},
abstract = {We introduce a way of relativizing operational set theory that also
takes care of application. After presenting the basic approach and
proving some essential properties of this new form of relativization we
turn to the notion of relativized regularity and to the system OST(LR)
that extends OST by a limit axiom claiming that any set is element
of a relativized regular set. Finally we show that OST(LR) is proof-
theoretically equivalent to the well-known theory KPi for a recursively
inaccessible universe.
},
issn = {1079-8986},
url = {http://www.iam.unibe.ch/ltgpub/2015/jae15.pdf},
author = {Gerhard J{\"a}ger}
}
@article {1792,
title = {Reverse mathematical bounds for the Termination Theorem},
journal = {Annals of Pure and Applied Logic},
year = {2016},
abstract = {Abstract In 2004 Podelski and Rybalchenko expressed the termination of transition-based programs as a property of well-founded relations. The classical proof by Podelski and Rybalchenko requires Ramsey{\textquoteright}s Theorem for pairs which is a purely classical result, therefore extracting bounds from the original proof is non-trivial task. Our goal is to investigate the termination analysis from the point of view of Reverse Mathematics. By studying the strength of Podelski and Rybalchenko{\textquoteright}s Termination Theorem we can extract some information about termination bounds.},
issn = {0168-0072},
doi = {10.1016/j.apal.2016.06.001},
url = {http://www.iam.unibe.ch/ltgpub/2016/styo16.pdf},
author = {Silvia Steila and Keita Yokoyama}
}
@article {Kuznets01062016,
title = {Weak arithmetical interpretations for the Logic of Proofs},
journal = {Logic Journal of IGPL},
volume = {24},
number = {3},
year = {2016},
pages = {424-440},
abstract = {Artemov established an arithmetical interpretation for the Logics of Proofs LPCS, which yields a classical provability semantics for the modal logic S4. The Logics of Proofs are parameterized by so-called constant specifications CS, stating which axioms can be used in the reasoning process, and the arithmetical interpretation relies on constant specifications being finite. In this article, we remove this restriction by introducing weak arithmetical interpretations that are sound and complete for a wide class of constant specifications, including infinite ones. In particular, they interpret the full Logic of Proofs LP.},
url = {http://www.iam.unibe.ch/ltgpub/2016/kust16.pdf},
author = {Roman Kuznets and Thomas Studer}
}
@article {sz14,
title = {A new model construction by making a detour via intuitionistic theories I: Operational set theory without choice is $\Pi$1-equivalent to KP},
journal = {Annals of pure and applied logic},
volume = {166},
number = {2},
year = {2015},
pages = {121-186},
publisher = {Elsevier},
abstract = {We introduce a version of operational set theory, OST?, without a choice operation, which has a machinery for {$Δ$}0{$Δ$}0 separation based on truth functions and the separation operator, and a new kind of applicative set theory, so-called weak explicit set theory WEST, based on G{\"o}del operations. We show that both the theories and Kripke?Platek set theory KPKP with infinity are pairwise {$\Pi$}1{$\Pi$}1 equivalent. We also show analogous assertions for subtheories with ?-induction restricted in various ways and for supertheories extended by powerset, beta, limit and Mahlo operations. Whereas the upper bound is given by a refinement of inductive definition in KPKP, the lower bound is by a combination, in a specific way, of realisability, (intuitionistic) forcing and negative interpretations. Thus, despite interpretability between classical theories, we make ?a detour via intuitionistic theories?. The combined interpretation, seen as a model construction in the sense of Visser{\textquoteright}s miniature model theory, is a new way of construction for classical theories and could be said the third kind of model construction ever used which is non-trivial on the logical connective level, after generic extension {\`a} la Cohen and Krivine{\textquoteright}s classical realisability model.},
url = {http://www.iam.unibe.ch/ltgpub/2014/sz14.pdf},
author = {Kentaro Sato and Rico Zumbrunnen}
}
@article {sat15b,
title = {A new model construction by making a detour via intuitionistic theories II: Interpretability lower bound of Feferman{\textquoteright}s explicit mathematics T0},
journal = {Annals of pure and applied logic},
volume = {166},
number = {7-8},
year = {2015},
pages = {800-835},
publisher = {Elsevier},
abstract = {We partially solve a long-standing problem in the proof theory of explicit mathematics or the proof theory in general. Namely, we give a lower bound of Feferman?s system T0 of explicit mathematics (but only when formulated on classical logic) with a concrete interpretat ion of the subsystem {$Σ$}12-AC+ (BI) of second order arithmetic inside T0. Whereas a lower bound proof in the sense of proof-theoretic reducibility or of ordinalanalysis was already given in 80s, the lower bound in the sense of interpretability we give here is new. We apply the new interpretation method developed by the author and Zumbrunnen (2015), which can be seen as the third kind of model construction method for classical theories, after Cohen?s forcing and Krivine?s classical realizability. It gives us an interpretation between classical theories, by composing interpretations between intuitionistic theories.},
url = {http://www.iam.unibe.ch/ltgpub/2015/sat15b.pdf},
author = {Kentaro Sato}
}
@article {ebat15,
title = {Applicative theories for logarithmic complexity classes},
journal = {Theoretical Computer Science},
volume = {585},
year = {2015},
month = {June},
pages = {115-135},
publisher = {Elsevier},
abstract = {We present applicative theories of words corresponding to weak, and especially logarithmic, complexity classes. The theories for the logarithmic hierarchy and alternating logarithmic time formalise function algebras with concatenation recursion as main principle. We present two theories for logarithmic space where the first formalises a new two-sorted algebra which is very similar to Cook and Bellantoni{\textquoteright}s famous two-sorted algebra B for polynomial time [4]. The second theory describes logarithmic space by formalising concatenation- and sharply bounded recursion. All theories contain the predicates WW representing words, and VV representing temporary inaccessible words. They are inspired by Cantini{\textquoteright}s theories [6] formalising B.},
url = {http://www.iam.unibe.ch/ltgpub/2015/ebat15.pdf},
author = {Sebastian Eberhard}
}
@article {kmos15,
title = {First steps towards probabilistic justification logic},
journal = {Logic Journal of IGPL},
volume = {23},
number = {4},
year = {2015},
month = {June},
pages = {662-687},
publisher = {Oxford University Press},
abstract = {In this article, we introduce the probabilistic justification logic PJ, a logic in which we can reason about the probability of justification statements. We present its syntax and semantics, and establish a strong completeness theorem. Moreover, we investigate the relationship between PJ and the logic of uncertain justifications.},
url = {http://www.iam.unibe.ch/ltgpub/2015/kmos15.pdf},
author = {Ioannis Kokkinis and Petar Maksimovi{\'c} and Zoran Ognjanovi{\'c} and Thomas Studer}
}
@article {sat15a,
title = {Full and hat inductive definitions are equivalent in NBG},
journal = {Archive for Mathematical Logic},
volume = {54},
number = {1-2},
year = {2015},
pages = {75-112},
publisher = {Springer},
abstract = {A new research project has, quite recently, been launched to clarify how different, from systems in second order number theory extending ACA 0, those in second order set theory extending NBG (as well as those in n + 3-th order number theory extending the so-called Bernays?G{\"o}del expansion of full n + 2-order number theory etc.) are. In this article, we establish the equivalence between {$Δ$}10{$\backslash$}bf-LFP and {$Δ$}10{$\backslash$}bf-FP, which assert the existence of a least and of a (not necessarily least) fixed point, respectively, for positive elementary operators (or between {$Δ$}n+20{$\backslash$}bf-LFP and {$Δ$}n+20{$\backslash$}bf-FP). Our proof also shows the equivalence between ID 1 and {\^{ }}ID1, both of which are defined in the standard way but with the starting theory PA replaced by ZFC (or full n + 2-th order number theory with global well-ordering).},
url = {http://www.iam.unibe.ch/ltgpub/2015/sat15a.pdf},
author = {Kentaro Sato}
}
@article {fkm15,
title = {Modal interpolation via nested sequents},
journal = {Annals of pure and applied logic},
volume = {166},
number = {3},
year = {2015},
month = {March},
pages = {274-305},
publisher = {Elsevier},
abstract = {The main method of proving the Craig Interpolation Property (CIP) constructively uses cut-free sequent proof systems. Until now, however, no such method has been known for proving the CIP using more general sequent-like proof formalisms, such as hypersequents, nested sequents, and labelled sequents. In this paper, we start closing this gap by presenting an algorithm for proving the CIP for modal logics by induction on a nested-sequent derivation. This algorithm is applied to all the logics of the so-called modal cube.},
url = {http://www.iam.unibe.ch/ltgpub/2015/fkm15.pdf},
author = {Melvin Fitting and Roman Kuznets}
}
@article {ebe12a,
title = {A feasible theory of truth over combinatory algebra},
journal = {Annals of Pure and Applied Logic},
volume = {165},
number = {5},
year = {2014},
pages = {1009-1033},
keywords = {Truth theories},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.12.002},
url = {http://www.iam.unibe.ch/ltgpub/2012/ebe12a.pdf},
author = {Sebastian Eberhard}
}
@article {rs13,
title = {A note on the theory $\mathsf{SID}_{{<}\omega}$ of stratified induction},
journal = {Mathematical Logic Quarterly},
volume = {60},
number = {6},
year = {2014},
pages = {487-497},
issn = {1521-3870},
doi = {10.1002/malq.201300063},
url = {http://www.iam.unibe.ch/ltgpub/2013/rs13.pdf},
author = {Ranzi, Florian and Thomas Strahm}
}
@article {sw14,
title = {Censors for Boolean Description Logic},
journal = {Transactions on Data Privacy},
volume = {7},
year = {2014},
pages = {223-252},
issn = {1888-5063},
url = {http://www.iam.unibe.ch/ltgpub/2014/sw14.pdf},
author = {Thomas Studer and Johannes Werner}
}
@article {jz14,
title = {Explicit mathematics and operational set theory: some ontological comparisons},
journal = {The Bulletin of Symbolic Logic},
volume = {20},
year = {2014},
month = {9},
pages = {275-292},
issn = {1943-5894},
doi = {10.1017/bsl.2014.21},
url = {http://www.iam.unibe.ch/ltgpub/2014/jz14.pdf},
author = {Gerhard J{\"a}ger and Rico Zumbrunnen}
}
@article {sat14,
title = {Forcing for Hat Inductive Definitions in Arithmetic {\textendash} One of the Simplest Applications of Forcing {\textendash}},
journal = {Mathematical Logic Quarterly},
volume = {60},
number = {4-5},
year = {2014},
pages = {314-318},
abstract = {By forcing, we give a direct interpretation of $\widehat{\mathsf{ID}}_\omega$ into Avigad{\textquoteright}s $\mathsf{FP}$. To the best of the author{\textquoteright}s knowledge, this is one of the simplest applications of forcing to {\textquoteleft}{\textquoteleft}real problems{\textquoteright}{\textquoteright}.},
issn = {1521-3870},
doi = {10.1002/malq.201300044},
url = {http://www.iam.unibe.ch/ltgpub/2014/sat14.pdf},
author = {Kentaro Sato}
}
@article {fs14,
title = {From hierarchies to well-foundedness},
journal = {Archive for Mathematical Logic},
volume = {53},
number = {7{\textendash}8},
year = {2014},
publisher = {Springer Berlin Heidelberg},
issn = {0933-5846},
doi = {10.1007/s00153-014-0392-9},
url = {http://www.iam.unibe.ch/ltgpub/2014/fs14.pdf},
author = {Dandolo Flumini and Kentaro Sato}
}
@article {aks14,
title = {Justifying induction on modal $μ$-formulae},
journal = {Logic Journal of IGPL},
volume = {22},
year = {2014},
pages = {805-817},
abstract = {We define a rank function for formulae of the propositional modal $\mu$-calculus such that the rank of a fixed point is strictly bigger than the rank of any of its finite approximations. A rank function of this kind is needed, for instance, to establish the collapse of the modal $\mu$-hierarchy over transitive transition systems. We show that the range of the rank function is $\omega^\omega$. Further we establish that the rank is computable by primitive recursion, which gives us a uniform method to generate formulae of arbitrary rank below $\omega^\omega$.},
doi = {10.1093/jigpal/jzu001},
url = {http://www.iam.unibe.ch/ltgpub/2014/aks14.pdf},
author = {Alberucci, Luca and Kr{\"a}henb{\"u}hl, J{\"u}rg and Thomas Studer}
}
@article {ak13,
title = {Logical Omniscience As Infeasibility},
journal = {Annals of Pure and Applied Logic},
volume = {165},
number = {1},
year = {2014},
pages = {6-25},
abstract = {Abstract Logical theories for representing knowledge are often plagued by the so-called Logical Omniscience Problem. The problem stems from the clash between the desire to model rational agents, which should be capable of simple logical inferences, and the fact that any logical inference, however complex, almost inevitably consists of inference steps that are simple enough. This contradiction points to the fruitlessness of trying to solve the Logical Omniscience Problem qualitatively if the rationality of agents is to be maintained. We provide a quantitative solution to the problem compatible with the two important facets of the reasoning agent: rationality and resource boundedness. More precisely, we provide a test for the logical omniscience problem in a given formal theory of knowledge. The quantitative measures we use are inspired by the complexity theory. We illustrate our framework with a number of examples ranging from the traditional implicit representation of knowledge in modal logic to the language of justification logic, which is capable of spelling out the internal inference process. We use these examples to divide representations of knowledge into logically omniscient and not logically omniscient, thus trying to determine how much information about the reasoning process needs to be present in a theory to avoid logical omniscience.},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.07.003},
url = {http://www.iam.unibe.ch/ltgpub/2013/ak13.pdf},
author = {Sergei Artemov and Roman Kuznets}
}
@article {sav13a,
title = {Proof Internalization for Generalized Frege Systems for Classical Logic},
journal = {Annals of Pure and Applied Logic},
volume = {165},
number = {1},
year = {2014},
pages = {340-356},
abstract = {Abstract We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.07.017},
url = {http://www.iam.unibe.ch/ltgpub/2013/sav13a.pdf},
author = {Yury Savateev}
}
@article {bks12a,
title = {Realizing Public Announcements by Justifications},
journal = {Journal of Computer and System Sciences},
volume = {80},
number = {6},
year = {2014},
pages = {1046-1066},
abstract = {Modal public announcement logics study how beliefs change after public announcements. However, these logics cannot express the reason for a new belief. Justification logics fill this gap since they can formally represent evidence and justifications for an agent{\textquoteright}s belief. We present ${\sf OPAL(K)}$ and ${\sf JPAL(K)}$, two alternative justification counterparts of Gerbrandy{\textendash}Groeneveld{\textquoteright}s public announcement logic ${\sf PAL(K)}$. We show that ${\sf PAL(K)}$ is the forgetful projection of both ${\sf OPAL(K)}$ and ${\sf JPAL(K)}$. We also establish that ${\sf JPAL(K)}$ partially realizes ${\sf PAL(K)}$. The question whether a similar result holds for ${\sf OPAL(K)}$ is still open.},
keywords = {Belief revision, Dynamic epistemic logic, justification logic, Public announcements},
doi = {10.1016/j.jcss.2014.04.001},
url = {http://www.iam.unibe.ch/ltgpub/2012/bks12a.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer}
}
@article {sat12,
title = {Relative predicativity and dependent recursion in second-order set theory and higher-order theories},
journal = {The Journal of Symbolic Logic},
volume = {79},
year = {2014},
month = {9},
pages = {712-732},
issn = {1943-5886},
doi = {10.1017/jsl.2014.28},
url = {http://www.iam.unibe.ch/ltgpub/2012/sat12.pdf},
author = {Kentaro Sato}
}
@article {stu12b,
title = {A Universal Approach to Guarantee Data Privacy},
journal = {Logica Universalis},
volume = {7},
number = {2},
year = {2013},
pages = {195-209},
url = {http://www.iam.unibe.ch/ltgpub/2012/stu12b.pdf},
author = {Thomas Studer}
}
@article {mck12a,
title = {Canonical proof nets for classical logic},
journal = {Annals of Pure and Applied Logic},
volume = {164},
number = {6},
year = {2013},
pages = {702-732},
issn = {0168-0072},
doi = {10.1016/j.apal.2012.05.007},
url = {http://www.iam.unibe.ch/ltgpub/2012/mck12a.pdf},
author = {Richard McKinley}
}
@article {stu13,
title = {Decidability for some justification logics with negative introspection},
journal = {The Journal of Symbolic Logic},
volume = {78},
number = {2},
year = {2013},
pages = {388-402},
url = {http://www.iam.unibe.ch/ltgpub/2013/stu13.pdf},
author = {Thomas Studer}
}
@article {jae13,
title = {Operational closure and stability},
journal = {Annals of Pure and Applied Logic},
volume = {164},
number = {7{\textendash}8},
year = {2013},
pages = {813-821},
abstract = {In this article we introduce and study the notion of operational closure: a transitive set d is called operationally closed iff it contains all constants of $\mathsf{OST}$ and any operation $f\in d$ applied to an element $a\in d$ yields an element $fa\in d$ , provided that $f$ applied to a has a value at all. We will show that there is a direct relationship between operational closure and stability in the sense that operationally closed sets behave like $\Sigma_1$ substructures of the universe. This leads to our final result that $\mathsf{OST}$ plus the axiom $(\mathsf{OLim})$ , claiming that any set is element of an operationally closed set, is proof-theoretically equivalent to the system $\mathsf{KP}+(\Sigma_1\text{-}\mathsf{Sep})$ of Kripke-Platek set theory with infinity and $\Sigma_1$ separation. We also characterize the system $\mathsf{OST}$ plus the existence of one operationally closed set in terms of Kripke-Platek set theory with infinity and a parameter-free version of $\Sigma_1$ separation.},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.01.004},
url = {http://www.iam.unibe.ch/ltgpub/2013/jae13.pdf},
author = {Gerhard J{\"a}ger}
}
@article {mck12b,
title = {Proof Nets for Herbrand{\textquoteright}s Theorem},
journal = {ACM Transactions on Computational Logic},
volume = {14},
number = {1},
year = {2013},
pages = {5},
doi = {10.1145/2422085.2422090},
url = {http://www.iam.unibe.ch/ltgpub/2012/mck12b.pdf},
author = {Richard McKinley}
}
@article {1313,
title = {Lower complexity bounds in justification logic},
journal = {Annals of Pure and Applied Logic},
volume = {163},
year = {2012},
note = {Published online November~2011},
pages = {888-905},
abstract = {Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in~NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound. The proof method is then extended to provide a uniform proof that the corresponding full pure justification logics are $\Pi^p_2$-hard, reproving and generalizing an earlier result by Milnikel.},
keywords = {Logic of Proofs},
doi = {10.1016/j.apal.2011.09.010},
url = {http://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/APAL09_final.pdf},
author = {Buss, Samuel R. and Roman Kuznets}
}
@article {1314,
title = {Product-free Lambek calculus is NP-complete},
journal = {Annals of Pure and Applied Logic},
volume = {163},
year = {2012},
note = {The Symposium on Logical Foundations of Computer Science 2009},
pages = {775-788},
doi = {10.1016/j.apal.2011.09.017},
url = {http://www.iam.unibe.ch/ltgpub/2012/sav12.pdf},
author = {Yury Savateev}
}
@article {1306,
title = {Realization for Justification Logics via Nested Sequents: Modularity through Embedding},
journal = {Annals of Pure and Applied Logic},
volume = {163},
year = {2012},
month = {September},
pages = {1271-1298},
doi = {10.1016/j.apal.2012.02.002},
url = {http://www.iam.unibe.ch/ltgpub/2012/gk12.pdf},
author = {Remo Goetschi and Roman Kuznets}
}
@article {bs12,
title = {Syntactic cut-elimination for a fragment of the modal mu-calculus},
journal = {Annals of Pure and Applied Logic},
volume = {163},
number = {12},
year = {2012},
pages = {1838-1853},
url = {http://www.iam.unibe.ch/ltgpub/2012/bs12.pdf},
author = {Kai Br{\"u}nnler and Thomas Studer}
}
@article {1319,
title = {A Buchholz rule for modal fixed point logics},
journal = {Logica Universalis},
volume = {5},
year = {2011},
note = {To appear, 2010},
pages = {1-19},
doi = {10.1007/s11787-010-0022-1},
url = {http://www.iam.unibe.ch/ltgpub/2011/js11.pdf},
author = {Gerhard J{\"a}ger and Thomas Studer}
}
@article {1317,
title = {Admissible closures of polynomial time computable arithmetic},
journal = {Archive for Mathematical Logic},
volume = {50},
year = {2011},
note = {Submitted, 2010},
pages = {643-660},
url = {http://www.iam.unibe.ch/ltgpub/2011/ps11.pdf},
author = {Dieter Probst and Thomas Strahm}
}
@article {1320,
title = {Justification Logic, Inference Tracking, and Data Privacy},
journal = {Logic and Logical Philosophy},
volume = {20},
year = {2011},
pages = {297-306},
url = {http://www.iam.unibe.ch/ltgpub/2011/stu11a.pdf},
author = {Thomas Studer}
}
@article {1321,
title = {Justifications for Common Knowledge},
journal = {Journal of Applied Non-classical Logics},
volume = {21},
year = {2011},
note = {To appear, 2011},
pages = {35-60},
doi = {10.3166/JANCL.21.35-60},
url = {http://www.iam.unibe.ch/ltgpub/2011/bks11a.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Valentin Goranko and Wojtek Jamroga}
}
@article {1324,
title = {Realizability in weak systems of explicit mathematics},
journal = {Mathematical Logic Quarterly},
volume = {57},
year = {2011},
note = {To appear, 2010},
pages = {551-565},
url = {http://www.iam.unibe.ch/ltgpub/2011/ss11.pdf},
author = {Spescha, Daria and Thomas Strahm}
}
@article {1323,
title = {The provably terminating operations of the subsystem PETJ of explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {162},
year = {2011},
note = {Submitted, 2010},
pages = {934-947},
doi = {10.1016/j.apal.2011.04.004},
url = {http://www.iam.unibe.ch/ltgpub/2011/pro11.pdf},
author = {Dieter Probst}
}
@article {1316,
title = {The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories},
journal = {Annals of Pure and Applied logic},
volume = {162},
year = {2011},
month = {2011},
pages = {647-660},
keywords = {Suslin operator in applicative theories},
doi = {10.1016/j.apal.2011.01.009},
url = {http://www.iam.unibe.ch/ltgpub/2011/jp11.pdf},
author = {Gerhard J{\"a}ger and Dieter Probst}
}
@article {1328,
title = {Self-Referential Justifications in Epistemic Logic},
journal = {Theory of Computing Systems},
volume = {46},
year = {2010},
month = {may},
pages = {636-661},
abstract = {This paper is devoted to the study of self-referential proofs and/or justifications, i.e., valid proofs that prove statements about these same proofs. The goal is to investigate whether such self-referential justifications are present in the reasoning described by standard modal epistemic logics such as~$\mathsf{S4}$. We argue that the modal language by itself is too coarse to capture this concept of self-referentiality and that the language of justification logic can serve as an adequate refinement. We consider well-known modal logics of knowledge/belief and show, using explicit justifications, that~$\mathsf{S4}$, $\mathsf{D4}$, $\mathsf{K4}$, and~$\mathsf{T}$ with their respective justification counterparts~$\mathsf{LP}$, $\mathsf{JD4}$, $\mathsf{J4}$, and~$\mathsf{JT}$ describe knowledge that is self-referential in some strong sense. We also demonstrate that self-referentiality can be avoided for~$\mathsf{K}$ and~$\mathsf{D}$. In order to prove the former result, we develop a machinery of minimal evidence functions used to effectively build models for justification logics. We observe that the calculus used to construct the minimal functions axiomatizes the reflected fragments of justification logics. We also discuss difficulties that result from an introduction of negative introspection.},
keywords = {self-referentiality},
doi = {10.1007/s00224-009-9209-3},
url = {http://www.iam.unibe.ch/ltgpub/2010/kuz10.pdf},
author = {Roman Kuznets}
}
@article {1343,
title = {Unfolding finitist arithmetic},
journal = {Review of Symbolic Logic},
volume = {3},
year = {2010},
pages = {665-689},
url = {http://www.iam.unibe.ch/ltgpub/2010/fs10.pdf},
author = {Solomon Feferman and Thomas Strahm}
}
@article {1360,
title = {Common knowledge does not have the Beth property},
journal = {Information Processing Letters},
volume = {109},
year = {2009},
pages = {611-614},
url = {http://www.iam.unibe.ch/ltgpub/2009/stu09.pdf},
author = {Thomas Studer}
}
@article {1347,
title = {Deep Sequent Systems for Modal Logic},
journal = {Archive for Mathematical Logic},
volume = {48},
year = {2009},
pages = {551-577},
doi = {10.1007/s00153-009-0137-3},
url = {http://www.iam.unibe.ch/ltgpub/2009/bru09.pdf},
author = {Kai Br{\"u}nnler}
}
@article {1362,
title = {Elementary explicit types and polynomial time operations},
journal = {Mathematical Logic Quarterly},
volume = {55},
year = {2009},
pages = {245-258},
url = {http://www.iam.unibe.ch/ltgpub/2009/ss09a.pdf},
author = {Spescha, Daria and Thomas Strahm}
}
@article {1363,
title = {Full operational set theory with unbounded existential quantification and power set},
journal = {Annals of Pure and Applied Logic},
volume = {160},
year = {2009},
pages = {33-52},
url = {http://www.iam.unibe.ch/ltgpub/2009/jae09a.pdf},
author = {Gerhard J{\"a}ger}
}
@article {1352,
title = {On modal $μ$-calculus and G{\"o}del-L{\"o}b logic},
journal = {Studia Logica},
volume = {91},
year = {2009},
pages = {145-169},
url = {http://www.iam.unibe.ch/ltgpub/2009/af09a.pdf},
author = {Luca Alberucci and Alessandro Facchini}
}
@article {1355,
title = {Sequent calculi for the modal $μ$-calculus over $\mathsf {S5}$},
journal = {Journal of Logic and Computation},
year = {2009},
note = {Published online on January 22, 2009},
url = {http://www.iam.unibe.ch/ltgpub/2009/alb09.pdf},
author = {Luca Alberucci}
}
@article {1356,
title = {Syntactic cut-elimination for common knowledge},
journal = {Annals of Pure and Applied Logic},
volume = {160},
year = {2009},
pages = {82-95},
doi = {10.1016/j.apal.2009.01.014},
url = {http://www.iam.unibe.ch/ltgpub/2009/bs09b.pdf},
author = {Kai Br{\"u}nnler and Thomas Studer}
}
@article {1350,
title = {The modal $μ$-calculus hierarchy over restricted classes of transition systems},
journal = {Journal of Symbolic Logic},
volume = {74},
year = {2009},
pages = {1367-1400},
url = {http://www.iam.unibe.ch/ltgpub/2009/af09b.pdf},
author = {Luca Alberucci and Alessandro Facchini}
}
@article {1367,
title = {Canonical completeness of infinitary mu},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
year = {2008},
pages = {270-292},
doi = {10.1016/j.jlap.2008.02.005},
url = {http://www.iam.unibe.ch/ltgpub/2008/jks08.pdf},
author = {Gerhard J{\"a}ger and Mathis Kretz and Thomas Studer}
}
@article {1368,
title = {Cut-free sequent systems for temporal logic},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
year = {2008},
pages = {216-225},
doi = {10.1016/j.jlap.2008.02.004},
url = {http://www.iam.unibe.ch/ltgpub/2008/bl08.pdf},
author = {Kai Br{\"u}nnler and Lange, Martin}
}
@article {1371,
title = {Introduction},
journal = {Dialectica},
volume = {62},
year = {2008},
pages = {145-147},
doi = {10.1111/j.1746-8361.2008.01143.x},
url = {http://www.iam.unibe.ch/ltgpub/2008/str08b.pdf},
author = {Thomas Strahm}
}
@article {1376,
title = {On contraction and the modal fragment},
journal = {Mathematical Logic Quarterly},
volume = {54},
year = {2008},
pages = {345-349},
url = {http://www.iam.unibe.ch/ltgpub/2008/bps08.pdf},
author = {Kai Br{\"u}nnler and Dieter Probst and Thomas Studer}
}
@article {1372,
title = {On the proof theory of the modal mu-calculus},
journal = {Studia Logica},
volume = {89},
year = {2008},
pages = {343-363},
doi = {10.1007/s11225-008-9133-6},
url = {http://www.iam.unibe.ch/ltgpub/2008/stu08.pdf},
author = {Thomas Studer}
}
@article {1377,
title = {Primitive recursive selection functions for existential assertions over abstract algebras},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
year = {2008},
pages = {175-197},
url = {http://www.iam.unibe.ch/ltgpub/2008/sz08.pdf},
author = {Thomas Strahm and Zucker, Jeffery I}
}
@article {1378,
title = {Soft linear set theory},
journal = {Journal of Logic and Algebraic Programming},
volume = {76},
year = {2008},
pages = {226-245},
url = {http://www.iam.unibe.ch/ltgpub/2008/mck08.pdf},
author = {Richard McKinley}
}
@article {1380,
title = {A deep inference system for the modal logic $\mathsf S5$},
journal = {Studia Logica},
volume = {85},
year = {2007},
pages = {199-214},
doi = {10.1007/s11225-007-9028-y},
url = {http://www.iam.unibe.ch/ltgpub/2007/sto07.pdf},
author = {Phiniki Stouppa}
}
@article {1379,
title = {Cut-free common knowledge},
journal = {Journal of Applied Logic},
volume = {5},
year = {2007},
pages = {681-689},
doi = {10.1016/j.jal.2006.02.003},
url = {http://www.iam.unibe.ch/ltgpub/2007/jks07.pdf},
author = {Gerhard J{\"a}ger and Mathis Kretz and Thomas Studer}
}
@article {1381,
title = {On Feferman{\textquoteright}s operational set theory $\mathsf{OST}$},
journal = {Annals of Pure and Applied Logic},
volume = {150},
year = {2007},
pages = {19-39},
url = {http://www.iam.unibe.ch/ltgpub/2007/jae07.pdf},
author = {Gerhard J{\"a}ger}
}
@article {1388,
title = {Cut elimination inside a deep inference system for classical predicate logic},
journal = {Studia Logica},
volume = {82},
year = {2006},
pages = {51-71},
doi = {10.1007/s11225-006-6605-4},
url = {http://www.iam.unibe.ch/ltgpub/2006/bru06a.pdf},
author = {Kai Br{\"u}nnler}
}
@article {1389,
title = {Deduction chains for common knowledge},
journal = {Journal of Applied Logic},
volume = {4},
year = {2006},
pages = {331-357},
doi = {10.1016/j.jal.2005.06.011},
url = {http://www.iam.unibe.ch/ltgpub/2006/ks06.pdf},
author = {Mathis Kretz and Thomas Studer}
}
@article {1393,
title = {Locality for classical logic},
journal = {Notre Dame Journal of Formal Logic},
volume = {47},
year = {2006},
pages = {557-580},
doi = {10.1305/ndjfl/1168352668},
url = {http://www.iam.unibe.ch/ltgpub/2006/bru06d.pdf},
author = {Kai Br{\"u}nnler}
}
@article {1397,
title = {On the proof theory of type two functionals based on primitive recursive operations},
journal = {Mathematical Logic Quarterly},
volume = {52},
year = {2006},
pages = {237-252},
url = {http://www.iam.unibe.ch/ltgpub/2006/ss06.pdf},
author = {David Steiner and Thomas Strahm}
}
@article {1398,
title = {The proof-theoretic analysis of transfinitely iterated quasi least fixed points},
journal = {The Journal of Symbolic Logic},
volume = {71},
year = {2006},
pages = {721-746},
url = {http://www.iam.unibe.ch/ltgpub/2006/pro06.pdf},
author = {Dieter Probst}
}
@article {1403,
title = {About cut elimination for logics of common knowledge},
journal = {Annals of Pure and Applied Logic},
volume = {133},
year = {2005},
pages = {73-99},
doi = {10.1016/j.apal.2004.10.004},
url = {http://www.iam.unibe.ch/ltgpub/2005/aj05.pdf},
author = {Luca Alberucci and Gerhard J{\"a}ger}
}
@article {1410,
title = {Elementary Arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {133},
year = {2005},
pages = {275-292},
url = {http://www.iam.unibe.ch/ltgpub/2005/ow05.pdf},
author = {Geoffrey E. Ostrin and Stanley S. Wainer}
}
@article {1411,
title = {Explicit mathematics: power types and overloading},
journal = {Annals of Pure and Applied Logic},
volume = {134},
year = {2005},
pages = {284-302},
url = {http://www.iam.unibe.ch/ltgpub/2005/stu05a.pdf},
author = {Thomas Studer}
}
@article {1413,
title = {On the relationship between fixed points and iteration in admissible set theory without foundation},
journal = {Archive for Mathematical Logic},
volume = {44},
year = {2005},
pages = {561-580},
url = {http://www.iam.unibe.ch/ltgpub/2005/pro05a.pdf},
author = {Dieter Probst}
}
@article {1417,
title = {Reflections on reflections in explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {136},
year = {2005},
pages = {116-133},
url = {http://www.iam.unibe.ch/ltgpub/2005/js05.pdf},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1422,
title = {A proof-theoretic characterization of the basic feasible functionals},
journal = {Theoretical Computer Science},
volume = {329},
year = {2004},
pages = {159-176},
url = {http://www.iam.unibe.ch/ltgpub/2004/str04.pdf},
author = {Thomas Strahm}
}
@article {1421,
title = {An intensional fixed point theory over first order arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {128},
year = {2004},
pages = {197-213},
url = {http://www.iam.unibe.ch/ltgpub/2004/jae04.pdf},
author = {Gerhard J{\"a}ger}
}
@article {1419,
title = {On modal $μ$-calculus and non-well-founded set theory},
journal = {Journal of Philosophical Logic},
volume = {33},
year = {2004},
pages = {343-360},
url = {http://www.iam.unibe.ch/ltgpub/2004/as04.pdf},
author = {Luca Alberucci and Vincenzo Salipante}
}
@article {1423,
title = {Variation on a theme of Sch{\"u}tte},
journal = {Mathematical Logic Quarterly},
volume = {50},
year = {2004},
pages = {258-264},
url = {http://www.iam.unibe.ch/ltgpub/2004/jp04b.pdf},
author = {Gerhard J{\"a}ger and Dieter Probst}
}
@article {1426,
title = {Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe},
journal = {Annals of Pure and Applied Logic},
volume = {120},
year = {2003},
pages = {165-196},
url = {http://www.iam.unibe.ch/ltgpub/2003/tup03.ps},
author = {Sergei Tupailo}
}
@article {1424,
title = {The proof-theoretic analysis of $Σ^1_1$ transfinite dependent choice},
journal = {Annals of Pure and Applied Logic},
volume = {122},
year = {2003},
pages = {195-234},
url = {http://www.iam.unibe.ch/ltgpub/2003/rue03a.pdf},
author = {Christian R{\"u}ede}
}
@article {1427,
title = {Theories with self-application and computational complexity},
journal = {Information and Computation},
volume = {185},
year = {2003},
pages = {263-297},
url = {http://www.iam.unibe.ch/ltgpub/2003/str03.pdf},
author = {Thomas Strahm}
}
@article {1428,
title = {Universes in metapredicative analysis},
journal = {Archive for Mathematical Logic},
volume = {42},
year = {2003},
pages = {129-151},
url = {http://www.iam.unibe.ch/ltgpub/2003/rue03b.pdf},
author = {Christian R{\"u}ede}
}
@article {1429,
title = {Extending the system $\mathsf{T}_0$ of explicit mathematics: the limit and Mahlo axioms},
journal = {Annals of Pure and Applied Logic},
volume = {114},
year = {2002},
pages = {79-101},
url = {http://www.iam.unibe.ch/ltgpub/2002/js02b.pdf},
author = {Gerhard J{\"a}ger and Thomas Studer}
}
@article {1437,
title = {Intuitionistic fixed point theories for strictly positive operators},
journal = {Mathematical Logic Quarterly},
volume = {48},
year = {2002},
pages = {195-202},
url = {http://www.iam.unibe.ch/ltgpub/2002/rs02.pdf},
author = {Christian R{\"u}ede and Thomas Strahm}
}
@article {1436,
title = {Transfinite dependent choice and $\omega$-model reflection},
journal = {The Journal of Symbolic Logic},
volume = {67},
year = {2002},
pages = {1153-1168},
url = {http://www.iam.unibe.ch/ltgpub/2002/rue02.pdf},
author = {Christian R{\"u}ede}
}
@article {1438,
title = {Wellordering proofs for metapredicative Mahlo},
journal = {The Journal of Symbolic Logic},
volume = {67},
year = {2002},
pages = {260-278},
url = {http://www.iam.unibe.ch/ltgpub/2002/str02.pdf},
author = {Thomas Strahm}
}
@article {1443,
title = {A semantics for $\lambda^{\{\}}_{\mathsf str}$: a calculus with overloading and late-binding},
journal = {Journal of Logic and Computation},
volume = {11},
year = {2001},
pages = {527-544},
url = {http://www.iam.unibe.ch/ltgpub/2001/stu01a.pdf},
author = {Thomas Studer}
}
@article {1446,
title = {First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo},
journal = {The Journal of Symbolic Logic},
volume = {66},
year = {2001},
pages = {1073-1089},
url = {http://www.iam.unibe.ch/ltgpub/2001/jae01.pdf},
author = {Gerhard J{\"a}ger}
}
@article {1447,
title = {Formalizing non-termination of recursive programs},
journal = {Journal of Logic and Algebraic Programming},
volume = {49},
year = {2001},
pages = {1-14},
url = {http://www.iam.unibe.ch/ltgpub/2001/ks01.pdf},
author = {Reinhard Kahle and Thomas Studer}
}
@article {1448,
title = {How to normalize the Jay},
journal = {Theoretical Computer Science},
volume = {254},
year = {2001},
pages = {677-681},
url = {http://www.iam.unibe.ch/ltgpub/2001/ps01.pdf},
author = {Dieter Probst and Thomas Studer}
}
@article {1449,
title = {Realization of analysis into explicit mathematics},
journal = {The Journal of Symbolic Logic},
volume = {66},
year = {2001},
pages = {1848-1864},
url = {http://www.iam.unibe.ch/ltgpub/2001/tup01.pdf},
author = {Sergei Tupailo}
}
@article {1450,
title = {Universes in explicit mathematics},
journal = {Annals of Pure and Applied Logic},
volume = {109},
year = {2001},
pages = {141-162},
url = {http://www.iam.unibe.ch/ltgpub/2001/jks01.pdf},
author = {Gerhard J{\"a}ger and Reinhard Kahle and Thomas Studer}
}
@article {1451,
title = {Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory},
journal = {The Journal of Symbolic Logic},
volume = {66},
year = {2001},
pages = {935-958},
url = {http://www.iam.unibe.ch/ltgpub/2001/js01.pdf},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1458,
title = {A benchmark method for the propositional modal logics K, KT, S4},
journal = {Journal of Automated Reasoning},
volume = {24},
year = {2000},
pages = {297-317},
url = {http://www.iam.unibe.ch/ltgpub/2000/bhs00.pdf},
author = {Peter Balsiger and Alain Heuerding and Stefan Schwendimann}
}
@article {1460,
title = {Fixed point theories and dependent choice},
journal = {Archive for Mathematical Logic},
volume = {39},
year = {2000},
pages = {493-508},
url = {http://www.iam.unibe.ch/ltgpub/2000/js00.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1456,
title = {N-strictness in applicative theories},
journal = {Archive for Mathematical Logic},
volume = {39},
year = {2000},
pages = {125-144},
doi = {10.1007/s001530050007},
url = {http://dx.doi.org/10.1007/s001530050007},
author = {Reinhard Kahle}
}
@article {1453,
title = {The non-constructive $μ$-operator, fixed point theories with ordinals, and the bar rule},
journal = {Annals of Pure and Applied Logic},
volume = {104},
year = {2000},
pages = {305-324},
url = {http://www.iam.unibe.ch/ltgpub/2000/str00b.ps},
author = {Thomas Strahm}
}
@article {1461,
title = {The unfolding of non-finitist arithmetic},
journal = {Annals of Pure and Applied Logic},
volume = {104},
year = {2000},
pages = {75-96},
url = {http://www.iam.unibe.ch/ltgpub/2000/fs00.ps},
author = {Solomon Feferman and Thomas Strahm}
}
@article {1462,
title = {Bar induction and $\omega$ model reflection},
journal = {Annals of Pure and Applied Logic},
volume = {97},
year = {1999},
pages = {221-230},
url = {http://www.iam.unibe.ch/ltgpub/1999/js99.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1473,
title = {The proof-theoretic analysis of transfinitely iterated fixed point theories},
journal = {The Journal of Symbolic Logic},
volume = {64},
year = {1999},
pages = {53-67},
url = {http://www.iam.unibe.ch/ltgpub/1999/jkss99.ps},
author = {Gerhard J{\"a}ger and Reinhard Kahle and Anton Setzer and Thomas Strahm}
}
@article {1479,
title = {Frege structures for partial applicative theories},
journal = {Journal of Logic and Computation},
volume = {8},
year = {1998},
pages = {683-700},
doi = {10.1093/logcom/9.5.683},
url = {http://dx.doi.org/10.1093/logcom/9.5.683},
author = {Reinhard Kahle}
}
@article {1474,
title = {The $μ$ quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals},
journal = {Archive for Mathematical Logic},
volume = {37},
year = {1998},
pages = {391-413},
url = {http://www.iam.unibe.ch/ltgpub/1998/ms98.ps},
author = {Markus Marzetta and Thomas Strahm}
}
@article {1491,
title = {Polynomial time operations in explicit mathematics},
journal = {The Journal of Symbolic Logic},
volume = {62},
year = {1997},
pages = {575-594},
url = {http://www.iam.unibe.ch/ltgpub/1997/str97.ps},
author = {Thomas Strahm}
}
@article {1492,
title = {Power types in explicit mathematics?},
journal = {The Journal of Symbolic Logic},
volume = {62},
year = {1997},
pages = {1142-1146},
url = {http://www.jstor.org/stable/2275630},
author = {Gerhard J{\"a}ger}
}
@article {1493,
title = {Relations between propositional normal modal logics: an overview},
journal = {Journal of Logic and Computation},
volume = {7},
year = {1997},
pages = {649-658},
url = {http://www.iam.unibe.ch/ltgpub/1997/ghh97.ps},
author = {Rajeev Gor{\'e} and Wolfgang Heinle and Alain Heuerding}
}
@article {1502,
title = {A logics workbench},
journal = {The European Journal on Artificial Intelligence},
volume = {9},
year = {1996},
pages = {53-58},
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan Schwendimann and Michael Seyfried}
}
@article {1506,
title = {LWBtheory: information about some propositional logics via the WWW},
journal = {Journal of the Interest Group in Pure and Applied Logic},
volume = {4},
year = {1996},
pages = {196-174},
url = {http://www.iam.unibe.ch/ltgpub/1996/heu96.ps},
author = {Alain Heuerding}
}
@article {1505,
title = {Partial applicative theories and explicit substitutions},
journal = {Journal of Logic and Computation},
volume = {6},
year = {1996},
pages = {55-77},
url = {http://www.iam.unibe.ch/ltgpub/1996/str96b.ps},
author = {Thomas Strahm}
}
@article {1496,
title = {Some theories with positive induction of ordinal strength $\varphi \omega 0$},
journal = {The Journal of Symbolic Logic},
volume = {61},
year = {1996},
pages = {818-842},
url = {http://www.iam.unibe.ch/ltgpub/1996/js96.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1497,
title = {Systems of explicit mathematics with non-constructive $μ$-operator and join},
journal = {Annals of Pure and Applied Logic},
volume = {82},
year = {1996},
pages = {193-219},
url = {http://www.iam.unibe.ch/ltgpub/1996/gs96.ps},
author = {Thomas Glass and Thomas Strahm}
}
@article {1498,
title = {Systems of explicit mathematics with non-constructive $μ$-operator. Part II},
journal = {Annals of Pure and Applied Logic},
volume = {79},
year = {1996},
pages = {37-52},
doi = {10.1016/0168-0072(95)00028-3},
url = {http://dx.doi.org/10.1016/0168-0072(95)00028-3},
author = {Solomon Feferman and Gerhard J{\"a}ger}
}
@article {1503,
title = {The logics workbench LWB: a snapshot},
journal = {Euromath Bulletin},
volume = {2},
year = {1996},
pages = {177-186},
url = {http://www.iam.unibe.ch/ltgpub/1996/hjss96b.ps},
author = {Alain Heuerding and Gerhard J{\"a}ger and Stefan Schwendimann and Michael Seyfried}
}
@article {1511,
title = {Second order theories with ordinals and elementary comprehension},
journal = {Archive for Mathematical Logic},
volume = {34},
year = {1995},
pages = {345-375},
url = {http://www.iam.unibe.ch/ltgpub/1995/js95a.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1512,
title = {Totality in applicative theories},
journal = {Annals of Pure and Applied Logic},
volume = {74},
year = {1995},
pages = {105-120},
url = {http://www.iam.unibe.ch/ltgpub/1995/js95b.ps},
author = {Gerhard J{\"a}ger and Thomas Strahm}
}
@article {1514,
title = {About some symmetries of negation},
journal = {The Journal of Symbolic Logic},
volume = {59},
year = {1994},
pages = {473-485},
url = {http://www.jstor.org/stable/2275401},
author = {Brigitte H{\"o}sli and Gerhard J{\"a}ger}
}
@article {1517,
title = {Fixed points in Peano arithmetic with ordinals},
journal = {Annals of Pure and Applied Logic},
volume = {60},
year = {1993},
pages = {119-132},
doi = {10.1016/0168-0072(93)90039-G},
url = {http://dx.doi.org/10.1016/0168-0072(93)90039-G},
author = {Gerhard J{\"a}ger}
}
@article {1518,
title = {Systems of explicit mathematics with non-constructive $μ$-operator. Part I},
journal = {Annals of Pure and Applied Logic},
volume = {65},
year = {1993},
pages = {243-263},
url = {http://www.iam.unibe.ch/ltgpub/1993/fj93.pdf},
author = {Solomon Feferman and Gerhard J{\"a}ger}
}
@article {1520,
title = {The defining power of stratified and hierarchical logic programs},
journal = {Journal of Logic Programming},
volume = {15},
year = {1993},
pages = {55-77},
url = {http://www.iam.unibe.ch/ltgpub/1993/js93.pdf},
author = {Gerhard J{\"a}ger and Robert F. St{\"a}rk}
}