{\rtf1\ansi\deff0\deftab360

{\fonttbl
{\f0\fswiss\fcharset0 Arial}
{\f1\froman\fcharset0 Times New Roman}
{\f2\fswiss\fcharset0 Verdana}
{\f3\froman\fcharset2 Symbol}
}

{\colortbl;
\red0\green0\blue0;
}

{\info
{\author Biblio 7.x}{\operator }{\title Biblio RTF Export}}

\f1\fs24
\paperw11907\paperh16839
\pgncont\pgndec\pgnstarts1\pgnrestart
 S.  Eberhard, ?Applicative theories for logarithmic complexity classes?. Submitted.\par \par  S.  Eberhard, ?A feasible theory of truth over combinatory logic?. Submitted.\par \par  K.  Sato, ?Full and Hat Inductive Definitions Are Equivalent in NBG?. Submitted.\par \par  K.  Sato, ?Relative Predicativity and Dependent Recursion in Second-order Set Theory and Higher-order Theories?. Submitted.\par \par  R.  McKinley, ?Canonical proof nets for classical logic?, Annals of Pure and Applied Logic (Special Issue: Classical Logic and Computation), In Press.\par \par  S.  Bucheli, R.  Kuznets, and T.  Studer, ?Decidability for Justification Logics Revisited?, in Selected papers of Ninth International Tbilisi Symposium on Language, Logic and Computation, In Press.\par \par  G.  J\'e4ger, ?Operational closure and stability?, Annals of Pure and Applied Logic, In Press.\par \par  R.  McKinley, ?Proof nets for Herbrand's Theorem?, ACM Transactions on Computational Logic, In Press.\par \par  S.  Bucheli, R.  Kuznets, and T.  Studer, ?Realizing Public Announcements by Justifications?, Journal of Computer and System Sciences, In Press.\par \par  S.  Eberhard and T.  Strahm, ?Unfolding feasible arithmetic and weak truth?, in Axiomatic Theories of Truth, In Press.\par \par  T.  Studer, ?A Universal Approach to Guarantee Data Privacy?, Logica Universalis, In Press.\par \par  S.  Bucheli, R.  Kuznets, and T.  Studer, ?Decidability for Justification Logics Revisited?, in Logic, Language, and Computation, 9th\'a0International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC\'a02011, Kutaisi, Georgia, September 26-30, 2011, Revised Selected Papers, vol. 7758, G.  Bezhanishvili, S.  L\'f6bner, V.  Marra, and F.  Richter Springer, 2013, pp. 166?181.\par \par  R.  Kuznets and T.  Studer, ?Update as Evidence: Belief Expansion?, in Logical Foundations of Computer Science, International Symposium, LFCS\'a02013, San Diego, CA, USA, January 6?8, 2013, Proceedings, vol. 7734, S.  Artemov and A.  Nerode Springer, 2013, pp. 266?279.\par \par  G.  J\'e4ger and R.  Zumbrunnen, ?About the Strength of Operational Regularity?, in Logic, Construction, Computation, 2012, pp. 305?324.\par \par  G.  Mints and T.  Studer, ?Cut-elimination for the mu-calculus with one variable?, in Fixed Points in Computer Science 2012, 2012, vol. 77, pp. 47?54.\par \par  R. P.  Kohler, ?Java-Programm zur interaktiven Bearbeitung von JALC-Herleitungen?. Universit\'e4t Bern, 2012.\par \par  S.  Bucheli, ?Justification Logics with Common Knowledge?. Universit\'e4t Bern, 2012.\par \par  R.  Kuznets and T.  Studer, ?Justifications, Ontology, and Conservativity?, in Advances in Modal Logic, volume 9, 2012, pp. 437?458.\par \par  T.  Studer, ?Justified Terminological Reasoning?, in Proceedings of Perspectives of System Informatics PSI'11, 2012, vol. 7162, pp. 349-361.\par \par  S. R.  Buss and R.  Kuznets, ?Lower complexity bounds in justification logic?, Annals of Pure and Applied Logic, vol. 163, pp. 888?905, 2012.\par \par  Y.  Savateev, ?Product-free Lambek calculus is NP-complete?, Annals of Pure and Applied Logic, vol. 163, pp. 775?788, 2012.\par \par  R.  Goetschi, ?On the Realization and Classification of Justification Logics?. Universit\'e4t Bern, 2012.\par \par  R.  Goetschi and R.  Kuznets, ?Realization for Justification Logics via Nested Sequents: Modularity through Embedding?, Annals of Pure and Applied Logic, vol. 163, pp. 1271?1298, 2012.\par \par  K.  Br\'fcnnler and T.  Studer, ?Syntactic cut-elimination for a fragment of the modal mu-calculus?, Annals of Pure and Applied Logic, vol. 163, pp. 1838?1853, 2012.\par \par  S.  Eberhard and T.  Strahm, ?Weak theories of truth and explicit mathematics?, in Logic, Construction, Computation, 2012, pp. 157?184.\par \par  D.  Probst and T.  Strahm, ?Admissible closures of polynomial time computable arithmetic?, Archive for Mathematical Logic, vol. 50, no. 5-6, pp. 643-660, 2011.\par \par  T.  Studer, ?An application of justification logic to protocol verification?, in Proceedings of Computational Intelligence and Security CIS 2011, 2011, p. 779\{?\}783.\par \par  D.  Fabian, ?Applicative theories on tree ordinal numbers?. Universit\'e4t Bern, 2011.\par \par  G.  J\'e4ger and T.  Studer, ?A Buchholz rule for modal fixed point logics?, Logica Universalis, vol. 5, no. 1, pp. 1-19, 2011.\par \par  T.  Studer, ?Justification Logic, Inference Tracking, and Data Privacy?, Logic and Logical Philosophy, vol. 20, pp. 297-306, 2011.\par \par  S.  Bucheli, R.  Kuznets, and T.  Studer, ?Justifications for Common Knowledge?, Journal of Applied Non-classical Logics, vol. 21, no. 1, pp. 35-60, 2011.\par \par  S.  Bucheli, R.  Kuznets, and T.  Studer, ?Partial Realization in Dynamic Justification Logic?, in Logic, Language, Information and Computation, 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, 2011, Proceedings, 2011, vol. 6642, pp. 35-51.\par \par  D.  Probst, ?The provably terminating operations of the subsystem PETJ of explicit mathematics?, Annals of Pure and Applied Logic, vol. 162, no. 11, pp. 934-947, 2011.\par \par  D.  Spescha and T.  Strahm, ?Realizability in weak systems of explicit mathematics?, Mathematical Logic Quarterly, vol. 57, no. 6, pp. 551-565, 2011.\par \par  J.  Kr\'e4henb\'fchl, ?On the Relationship between Choice Schemes and Iterated Class Comprehension in Set Theory?. Universit\'e4t Bern, 2011.\par \par  G.  J\'e4ger and D.  Probst, ?The Suslin operator in applicative theories: its proof-theoretic analysis via ordinal theories?, Annals of Pure and Applied logic, vol. 162, no. 8, pp. 647-660, 2011.\par \par  R.  Wehbe, ?Annotated Systems for Common Knowledge?. Universit\'e4t Bern, 2010.\par \par  R.  McKinley, ?Expansion nets: Proof nets for for propositional classical logic?, in Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 17), 2010, vol. 6397, pp. 535-549.\par \par  S.  Bucheli, R.  Kuznets, and T.  Studer, ?Explicit Evidence Systems with Common Knowledge?. arXiv.org, 2010.\par \par  S.  Bucheli, R.  Kuznets, B.  Renne, J.  Sack, and T.  Studer, ?Justified Belief Change?, in Proceedings of the \{S\}econd \{ILCLI\} \{I\}nternational \{W\}orkshop on \{L\}ogic and \{P\}hilosphy of \{K\}nowledge, \{C\}ommunication and \{A\}ction (\{L\}og\{KCA\}-10), 2010, pp. 135?155.\par \par  G.  J\'e4ger, ?Modal Fixed Point Logics?, in Logics and \{L\}anguages for \{R\}eliability and \{S\}ecurity, 2010, vol. 25.\par \par  K.  Br\'fcnnler, ?Nested Sequents?. Universit\'e4t Bern, 2010.\par \par  T.  Studer, ?Privacy Preserving Modules for Ontologies?, in Proceedings of \{P\}erspectives of \{S\}ystem \{I\}nformatics \{PSI\}'09, 2010, vol. 5947, p. 380\{?\}387.\par \par  J.  Brugger, ?Proof-theoretic aspects of weak K\'f6nig's Lemma?. Universit\'e4t Bern, 2010.\par \par  T.  Studer, ?Proof-Theoretic Contributions to Modal Fixed Point Logics?. Universit\'e4t Bern, 2010.\par \par  R.  Kuznets, ?Self-Referential Justifications in Epistemic Logic?, Theory of Computing Systems, vol. 46, pp. 636?661, 2010.\par \par  C.  Pulver, ?Self-Referentiality in Contraction-free Fragments of Modal Logic S4?. Universit\'e4t Bern, 2010.\par \par  K.  Br\'fcnnler, R.  Goetschi, and R.  Kuznets, ?A Syntactic Realization Theorem for Justification Logics?, in Advances in Modal Logic, Volume 8, 2010, pp. 39?58.\par \par  S.  Bucheli, R.  Kuznets, and T.  Studer, ?Two Ways to Common Knowledge?, in Proceedings of the 6th\'a0Workshop on \{M\}ethods for \{Modalities\} (\{M4M?6\'a02009\}), \{C\}openhagen, \{D\}enmark, 12?14 \{N\}ovember 2009, 2010, pp. 83?98.\par \par  S.  Feferman and T.  Strahm, ?Unfolding finitist arithmetic?, Review of Symbolic Logic, vol. 3, pp. 665?689, 2010.\par \par  M. C.  Stolz, ?Verification of Workflow Control-Flow Patterns with the SPIN Model Checker?. Universit\'e4t Bern, 2010.\par \par  T.  Strahm, ?Weak theories of operations and types?, in Ways of \{P\}roof \{T\}heory, 2010, pp. 441?468.\par \par  G.  J\'e4ger and J.  Kr\'e4henb\'fchl, ?$?^1_1$ choice in a theory of sets and classes?, in Ways of \{P\}roof \{T\}heory, 2010, pp. 283?314.\par \par  S.  Eberhard, ?Aspekte beweisbar totaler Funktionen in applikativen Theorien?. Universit\'e4t Bern, 2009.\par \par  D.  Steiner, ?Belief Change Functions for Multi-Agent Systems?. Universit\'e4t Bern, 2009.\par \par  T.  Studer, ?Common knowledge does not have the Beth property?, Information Processing Letters, vol. 109, pp. 611?614, 2009.\par \par  P.  Stouppa and T.  Studer, ?Data Privacy for ALC Knowledge Bases?, in Proceedings of \{L\}ogical \{F\}oundations of \{C\}omputer \{S\}cience \{LFCS\}'09, 2009, vol. 5407, pp. 409?421.\par \par  P.  Stouppa, ?Deciding Data Privacy for ALC Knowledge Bases?. Universit\'e4t Bern, 2009.\par \par  K.  Br\'fcnnler, ?Deep Sequent Systems for Modal Logic?, Archive for Mathematical Logic, vol. 48, pp. 551?577, 2009.\par \par  D.  Spescha and T.  Strahm, ?Elementary explicit types and polynomial time operations?, Mathematical Logic Quarterly, vol. 55, pp. 245 ?258, 2009.\par \par  G.  J\'e4ger, ?Full operational set theory with unbounded existential quantification and power set?, Annals of Pure and Applied Logic, vol. 160, pp. 33?52, 2009.\par \par  J.  Kr\'e4henb\'fchl, ?Justifying induction on modal mu-formulae?. Universit\'e4t Bern, 2009.\par \par  S.  Artemov and R.  Kuznets, ?Logical Omniscience as a Computational Complexity Problem?, in Theoretical \{A\}spects of \{R\}ationality and \{K\}nowledge, Proceedings of the Twelfth Conference (\{TARK\'a02009\}), Stanford University, California, 2009, pp. 14?23.\par \par  L.  Alberucci and A.  Facchini, ?On modal $?$-calculus and G\'f6del-L\'f6b logic?, Studia Logica, vol. 91, pp. 145-169, 2009.\par \par  L.  Alberucci and A.  Facchini, ?The modal $?$-calculus hierarchy over restricted classes of transition systems?, Journal of Symbolic Logic, vol. 74, pp. 1367?1400, 2009.\par \par  K.  Br\'fcnnler and L.  Stra\'dfburger, ?Modular Sequent Systems for Modal Logic?, in Tableaux 2009, 2009, vol. 5607.\par \par  R.  Kuznets, ?A Note on the Use of Sum in the Logic of Proofs?, in Proceedings of the 7th\'a0\{P\}anhellenic \{L\}ogic \{S\}ymposium, Patras University, Greece, 2009, pp. 99?103.\par \par  S. R.  Buss and R.  Kuznets, ?The NP-completeness of reflected fragments of justification logics?, in Proceedings of \{S\}ymposium on \{L\}ogical \{F\}oundations of \{C\}omputer \{S\}cience (\{LFCS\}'09), 2009, vol. 5407, pp. 122-136.\par \par  R.  Zumbrunnen, ?Ontological Questions about Operational Set Theory?. Universit\'e4t Bern, 2009.\par \par  G.  J\'e4ger, ?Operations, sets and classes?, in Logic, \{M\}ethodology and \{P\}hilosophy of \{S\}cience - \{P\}roceedings of the \{T\}hirteenth \{I\}nternational \{C\}ongress, 2009.\par \par  R.  Traber, ?Proof-Systems for PLTL: Cycling Sequents and their Use in a Finitization for PLTL?. Universit\'e4t Bern, 2009.\par \par  L.  Alberucci, ?Sequent calculi for the modal $?$-calculus over $\\mathsf \{S5\}$?, Journal of Logic and Computation, 2009.\par \par  K.  Br\'fcnnler and T.  Studer, ?Syntactic cut-elimination for common knowledge?, Annals of Pure and Applied Logic, vol. 160, pp. 82-95, 2009.\par \par  K.  Br\'fcnnler and T.  Studer, ?Syntactic cut-elimination for common knowledge?, in Proceedings of \{M\}ethods for \{M\}odalities \{M\}4\{M\}5, 2009, vol. 231, pp. 227?240.\par \par  D.  Spescha, ?Weak Systems of Explicit Mathematics?. Universit\'e4t Bern, 2009.\par \par  K.  Br\'fcnnler and R.  McKinley, ?An Algorithmic Interpretation of a Deep Inference System?, in LPAR 2008, 2008, vol. 5330, p. 482?-496.\par \par  C.  Larrzabal, ?Automatic Model Checking of UML models?. Universit\'e4t Bern, 2008.\par \par  S.  Liniger, ?The Basic Feasible Functionals in Bounded Arithmetic?. Universit\'e4t Bern, 2008.\par \par  G.  J\'e4ger, M.  Kretz, and T.  Studer, ?Canonical completeness of infinitary mu?, Journal of Logic and Algebraic Programming, vol. 76, pp. 270-292, 2008.\par \par  K.  Br\'fcnnler, D.  Probst, and T.  Studer, ?On contraction and the modal fragment?, Mathematical Logic Quarterly, vol. 54, pp. 345?349, 2008.\par \par  K.  Br\'fcnnler and M.  Lange, ?Cut-free sequent systems for temporal logic?, Journal of Logic and Algebraic Programming, vol. 76, pp. 216-225, 2008.\par \par  S.  Bucheli, ?Explicit Mathematics with Positive Existential Stratified Comprehension, Join and Uniform Monotone Inductive Definitions?. Universit\'e4t Bern, 2008.\par \par  T.  Strahm, G\'f6del's Dialectica Interpretation, Special. Wiley, 2008.\par \par  T.  Strahm, ?Introduction?, Dialectica, vol. 62, pp. 145?147, 2008.\par \par  R.  Goetschi, ?Polytime Functions in Two-Sorted Bounded Arithmetic?. Universit\'e4t Bern, 2008.\par \par  T.  Strahm and J. I.  Zucker, ?Primitive recursive selection functions for existential assertions over abstract algebras?, Journal of Logic and Algebraic Programming, vol. 76, pp. 175-197, 2008.\par \par  T.  Studer, ?On the proof theory of the modal mu-calculus?, Studia Logica, vol. 89, pp. 343?363, 2008.\par \par  R.  McKinley, ?Soft linear set theory?, Journal of Logic and Algebraic Programming, vol. 76, pp. 226-245, 2008.\par \par  R.  Wehbe, ?Computing with common knowledge?, in Proceedings of Artificial Intelligence and Soft Computing, 2007, p. 45\{?\}50.\par \par  G.  J\'e4ger, M.  Kretz, and T.  Studer, ?Cut-free common knowledge?, Journal of Applied Logic, vol. 5, p. 681\{?\}689, 2007.\par \par  P.  Stouppa, ?A deep inference system for the modal logic $\\mathsf S5$?, Studia Logica, vol. 85, p. 199\{?\}214, 2007.\par \par  G.  J\'e4ger, ?On Feferman's operational set theory $\\mathsf OST$?, Annals of Pure and Applied Logic, vol. 150, p. 19\{?\}39, 2007.\par \par  P.  Stouppa and T.  Studer, ?A formal model of data privacy?, in Proceedings of Perspectives of System Informatics, 2007, vol. 4378, p. 401\{?\}411.\par \par  N.  Kottmann and T.  Studer, ?Improving semantic query answering?, in Proceedings of Database and Expert Systems Applications, 2007, vol. 4653, p. 671\{?\}679.\par \par  R.  Wehbe, ?Merging rule-based belief databases?, in Proceedings of Artificial Intelligence and Applications, 2007, p. 585\{?\}589.\par \par  L.  Alberucci, ?A syntactical treatment of simultaneous fixpoints in the modal $?$-calculus?. Universit\'e4t Bern, 2007.\par \par  D.  Steiner and T.  Studer, ?Total public announcements?, in Proceedings of Logical Foundations of Computer Science, 2007, vol. 4514, p. 498\{?\}511.\par \par  K.  Br\'fcnnler, ?Cut elimination inside a deep inference system for classical predicate logic?, Studia Logica, vol. 82, p. 51\{?\}71, 2006.\par \par  M.  Kretz and T.  Studer, ?Deduction chains for common knowledge?, Journal of Applied Logic, vol. 4, p. 331\{?\}357, 2006.\par \par  K.  Br\'fcnnler, ?Deep inference and its normal form of derivations?, in Proceedings of Computability in Europe, 2006, vol. 3988, p. 65\{?\}74.\par \par  K.  Br\'fcnnler, ?Deep sequent systems for modal logic?, in Proceedings of Advances in Modal Logic, 2006, vol. 6, p. 107\{?\}119.\par \par  N.  Kottmann, ?Description Logic Query Answering with Relational Databases?. Universit\'e4t Bern, 2006.\par \par  J.  Kr\'e4henb\'fchl, ?Explicit Mathematics with Positive Existential Comprehension and Join?. Universit\'e4t Bern, 2006.\par \par  R.  Wehbe, ?A hybrid representation of knowledge and belief?, in Proceedings of Formal Approaches to Multi-Agent Systems, 2006.\par \par  K.  Br\'fcnnler, ?Locality for classical logic?, Notre Dame Journal of Formal Logic, vol. 47, p. 557\{?\}580, 2006.\par \par  D.  Steiner and T.  Strahm, ?On the proof theory of type two functionals based on primitive recursive operations?, Mathematical Logic Quarterly, vol. 52, p. 237\{?\}252, 2006.\par \par  D.  Probst, ?The proof-theoretic analysis of transfinitely iterated quasi least fixed points?, The Journal of Symbolic Logic, vol. 71, p. 721\{?\}746, 2006.\par \par  M.  Kretz, ?Proof-Theoretic Aspects of Modal Logic with Fixed Points?. Universit\'e4t Bern, 2006.\par \par  R.  Wehbe, ?Revising non-monotonic rule-based belief databases?, in Proceedings of Belief Revision, Belief Merging and Social Choice, 2006.\par \par  D.  Steiner, ?A system for consistency preserving belief change?, in Proceedings of Rationality and Knowledge, 2006, p. 133\{?\}144.\par \par  L.  Alberucci and G.  J\'e4ger, ?About cut elimination for logics of common knowledge?, Annals of Pure and Applied Logic, vol. 133, p. 73\{?\}99, 2005.\par \par  D.  Spescha, ?ALOE ? A Graphical Editor for OWL Ontologies?. Universit\'e4t Bern, 2005.\par \par  V.  Salipante, ?On the Consistency Strength of the Strict $\\Pi^1_1$ Reflection Principle?. Universit\'e4t Bern, 2005.\par \par  G.  J\'e4ger, M.  Kretz, and T.  Studer, ?Cut-free axiomatizations for stratified modal fixed point logic?, in Proceedings of Methods for Modalities 4, 2005, vol. 194, p. 125\{?\}143.\par \par  G. E.  Ostrin and S. S.  Wainer, ?Elementary Arithmetic?, Annals of Pure and Applied Logic, vol. 133, p. 275\{?\}292, 2005.\par \par  T.  Studer, ?Explicit mathematics: power types and overloading?, Annals of Pure and Applied Logic, vol. 134, p. 284\{?\}302, 2005.\par \par  M.  D\'fcrig, ?$\\mathcal\{PALC\}$: Extending $\\mathcal\{ALC\}$ ABoxes with Probabilities?. Universit\'e4t Bern, 2005.\par \par  D.  Sonderegger, ?$\\mathsf\{PLTL\}$ ? Vollst\'e4ndigkeit und Modell-Konstruktion?. Universit\'e4t Bern, 2005.\par \par  G.  J\'e4ger, ?Metapredicative and explicit Mahlo: a proof-theoretic perspective?, in Proceedings of Logic Colloquium '00, 2005, vol. 19, p. 272\{?\}293.\par \par  M.  D\'fcrig and T.  Studer, ?Probabilistic ABox reasoning: preliminary results?, in Proceedings of Description Logics '05, 2005, vol. 147, p. 104\{?\}111.\par \par  K.  Stoffel and T.  Studer, ?Provable data privacy?, in Proceedings of 16th International Conference on Database and Expert Systems Applications, 2005, vol. 3588, p. 324\{?\}332.\par \par  D.  Probst, ?Pseudo-Hierarchies in Admissible Set Theory without Foundation and Explicit Mathematics?. Universit\'e4t Bern, 2005.\par \par  G.  J\'e4ger and T.  Strahm, ?Reflections on reflections in explicit mathematics?, Annals of Pure and Applied Logic, vol. 136, p. 116\{?\}133, 2005.\par \par  T.  Studer, ?Relational representation of $\\mathcal\{ALN\}$ knowledge bases?, in Proceedings of Multi '05, 2005, p. 271\{?\}278.\par \par  D.  Probst, ?On the relationship between fixed points and iteration in admissible set theory without foundation?, Archive for Mathematical Logic, vol. 44, p. 561\{?\}580, 2005.\par \par  K.  Br\'fcnnler and S.  Lengrand, ?On two forms of bureaucracy in derivations?, in Proceedings of Structures and Deduction, 2005, p. 65\{?\}74.\par \par  M.  Wirz, ?Wellordering Two Sorts: A Slow-Growing Proof Theory for Variable Separation?. Universit\'e4t Bern, 2005.\par \par  G.  J\'e4ger, ?An intensional fixed point theory over first order arithmetic?, Annals of Pure and Applied Logic, vol. 128, p. 197\{?\}213, 2004.\par \par  G.  J\'e4ger and D.  Probst, ?Iterating $?$ operations in admissible set theory without foundation: a further aspect of metapredicative Mahlo?, in One Hundred Years of Russell's Paradox. Papers from the 2001 Munich Russell Conference, 2004, p. 119\{?\}134.\par \par  L.  Alberucci and V.  Salipante, ?On modal $?$-calculus and non-well-founded set theory?, Journal of Philosophical Logic, vol. 33, p. 343\{?\}360, 2004.\par \par  T.  Strahm, ?A proof-theoretic characterization of the basic feasible functionals?, Theoretical Computer Science, vol. 329, p. 159\{?\}176, 2004.\par \par  G.  J\'e4ger and D.  Probst, ?Variation on a theme of Sch\'fctte?, Mathematical Logic Quarterly, vol. 50, p. 258\{?\}264, 2004.\par \par  T.  Burri, ?Weak K\'f6nig's Lemma and Extensional Equality?. Universit\'e4t Bern, 2004.\par \par  C.  R\'fcede, ?The proof-theoretic analysis of $?^1_1$ transfinite dependent choice?, Annals of Pure and Applied Logic, vol. 122, p. 195\{?\}234, 2003.\par \par  S.  Tupailo, ?Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe?, Annals of Pure and Applied Logic, vol. 120, p. 165\{?\}196, 2003.\par \par  T.  Strahm, ?Theories with self-application and computational complexity?, Information and Computation, vol. 185, p. 263\{?\}297, 2003.\par \par  T.  Schweizer, ?Two Interpretations of $\\mathsf\{WKL\}_0$ in Subsystems of $\\mathsf\{PA\}$?. Universit\'e4t Bern, 2003.\par \par  C.  R\'fcede, ?Universes in metapredicative analysis?, Archive for Mathematical Logic, vol. 42, p. 129\{?\}151, 2003.\par \par  G.  J\'e4ger and T.  Studer, ?Extending the system $\\mathsf\{T\}_0$ of explicit mathematics: the limit and Mahlo axioms?, Annals of Pure and Applied Logic, vol. 114, p. 79\{?\}101, 2002.\par \par  P.  Keller, ?Information Flow ? Logics for the (R)age of Information?. Universit\'e4t Bern, 2002.\par \par  C.  R\'fcede and T.  Strahm, ?Intuitionistic fixed point theories for strictly positive operators?, Mathematical Logic Quarterly, vol. 48, p. 195\{?\}202, 2002.\par \par  L.  Alberucci, ?The Modal $?$-Calculus and the Logic of Common Knowledge?. Universit\'e4t Bern, 2002.\par \par  G. E.  Ostrin and S. S.  Wainer, ?Proof theoretic complexity?, in Proof and System Reliability, 2002, vol. 62, p. 369\{?\}398.\par \par  G.  J\'e4ger and T.  Strahm, ?The proof-theoretic analysis of the Suslin operator in applicative theories?, in Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, 2002, p. 270\{?\}292.\par \par  L.  Alberucci, ?Strictness of the modal $?$-calculus hierarchy?, in Automata, Logics and infinite Games: A Guide to Current Research, 2002, vol. 2500, p. 185\{?\}201.\par \par  C.  R\'fcede, ?Transfinite dependent choice and $\\omega$-model reflection?, The Journal of Symbolic Logic, vol. 67, p. 1153\{?\}1168, 2002.\par \par  M.  Kretz, ?On the Treatment of Predicative Polymorphism in Theories of Explicit Mathematics?. Universit\'e4t Bern, 2002.\par \par  T.  Strahm, ?Wellordering proofs for metapredicative Mahlo?, The Journal of Symbolic Logic, vol. 67, p. 260\{?\}278, 2002.\par \par  T.  Studer, ?Constructive foundations for Featherweight Java?, in Proceedings of the International Seminar on Proof Theory in Computer Science, 2001, vol. 2183, p. 202\{?\}238.\par \par  G.  J\'e4ger, ?First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo?, The Journal of Symbolic Logic, vol. 66, p. 1073\{?\}1089, 2001.\par \par  R.  Kahle and T.  Studer, ?Formalizing non-termination of recursive programs?, Journal of Logic and Algebraic Programming, vol. 49, p. 1\{?\}14, 2001.\par \par  D.  Probst and T.  Studer, ?How to normalize the Jay?, Theoretical Computer Science, vol. 254, pp. 677-681, 2001.\par \par  P.  Balsiger, ?The MacLWB and the Logic of Likelihood?. Universit\'e4t Bern, 2001.\par \par  T.  Studer, ?Object-Oriented Programming in Explicit Mathematics: Towards the Mathematics of Objects?. Universit\'e4t Bern, 2001.\par \par  T.  Strahm, ?Proof-theoretic contributions to explicit mathematics?. Universit\'e4t Bern, 2001.\par \par  D.  Steiner, ?Proof-Theoretic Strength of $\\mathsf\{PRON\}$ with Various Extensions?. Universit\'e4t Bern, 2001.\par \par  S.  Tupailo, ?Realization of analysis into explicit mathematics?, The Journal of Symbolic Logic, vol. 66, p. 1848\{?\}1864, 2001.\par \par  T.  Studer, ?A semantics for  $\\lambda^\{\\\{\\\}\}_\{\\mathsf str\}$: a calculus with overloading and late-binding?, Journal of Logic and Computation, vol. 11, p. 527\{?\}544, 2001.\par \par  M.  Heissenb\'fcttel, ?Theories of Ordinal Strength $\\varphi 2 0$ and $\\varphi 2 \\varepsilon_0$?. Universit\'e4t Bern, 2001.\par \par  G.  J\'e4ger, R.  Kahle, and T.  Studer, ?Universes in explicit mathematics?, Annals of Pure and Applied Logic, vol. 109, p. 141\{?\}162, 2001.\par \par  G.  J\'e4ger and T.  Strahm, ?Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory?, The Journal of Symbolic Logic, vol. 66, p. 935\{?\}958, 2001.\par \par  T.  Strahm, ?Autonomous fixed point progressions and fixed point transfinite recursion?, in Proceedings of Logic Colloquium '98, 2000, vol. 13, p. 449\{?\}464.\par \par  P.  Balsiger, A.  Heuerding, and S.  Schwendimann, ?A benchmark method for the propositional modal logics K, KT, S4?, Journal of Automated Reasoning, vol. 24, p. 297\{?\}317, 2000.\par \par  M.  Krebs, ?Einige Aspekte der Modallogik $\\mathsf\{S5\}_n$ mit Allgemeinwissen?. Universit\'e4t Bern, 2000.\par \par  S.  Tupailo, ?Finitary reductions for local predicativity, I: recursively regular ordinals?, in Proceedings of Logic Colloquium '98, 2000, vol. 13, p. 465\{?\}499.\par \par  G.  J\'e4ger and T.  Strahm, ?Fixed point theories and dependent choice?, Archive for Mathematical Logic, vol. 39, p. 493\{?\}508, 2000.\par \par  C.  R\'fcede, ?Metapredicative Subsystems of Analysis?. Universit\'e4t Bern, 2000.\par \par  T.  Strahm, ?The non-constructive $?$-operator, fixed point theories with ordinals, and the bar rule?, Annals of Pure and Applied Logic, vol. 104, p. 305\{?\}324, 2000.\par \par  R.  Kahle, ?N-strictness in applicative theories?, Archive for Mathematical Logic, vol. 39, p. 125\{?\}144, 2000.\par \par  R.  Kahle and T.  Studer, ?A theory of explicit mathematics equivalent to $\{ \\mathsf\{ID\} \}_1$?, in Proceedings of Computer Science Logic, 2000, vol. 1862, p. 356\{?\}370.\par \par  S.  Feferman and T.  Strahm, ?The unfolding of non-finitist arithmetic?, Annals of Pure and Applied Logic, vol. 104, p. 75\{?\}96, 2000.\par \par  G.  J\'e4ger, R.  Kahle, and T.  Strahm, ?On applicative theories?, in Logic and Foundations of Mathematics, 1999, p. 83\{?\}92.\par \par  G.  J\'e4ger and T.  Strahm, ?Bar induction and $\\omega$ model reflection?, Annals of Pure and Applied Logic, vol. 97, p. 221\{?\}230, 1999.\par \par  M.  Wirz, ?Characterizing the Grzegorczyk hierarchy by safe recursion?. Universit\'e4t Bern, 1999.\par \par  M.  Wirz, ?Charakterisierungen kleiner Komplexit\'e4tsklassen mittels geschichteter N-Pr\'e4dikate?. Universit\'e4t Bern, 1999.\par \par  D.  Probst, ?Dependent Choice in Explicit Mathematics?. Universit\'e4t Bern, 1999.\par \par  G.  Mints and S.  Tupailo, ?Epsilon-substitution method for the ramified language and $?^1_1$-comprehension rule?, in Logic and Foundation of Mathematics, 1999, p. 107\{?\}130.\par \par  I.  Bucher, ?Extension of the Modal System KT4?. Universit\'e4t Bern, 1999.\par \par  T.  Strahm, ?First steps into metapredicativity in explicit mathematics?, in Sets and Proofs, 1999, vol. 258, p. 383\{?\}402.\par \par  J.  Brignioni, ?Konstruktion von Gegenmodellen intuitionistisch unbeweisbarer Sequenzen?. Universit\'e4t Bern, 1999.\par \par  A. D.  Boroumand, ?Logics Workbench f\'fcr Window System?. Universit\'e4t Bern, 1999.\par \par  G.  J\'e4ger, R.  Kahle, A.  Setzer, and T.  Strahm, ?The proof-theoretic analysis of transfinitely iterated fixed point theories?, The Journal of Symbolic Logic, vol. 64, p. 53\{?\}67, 1999.\par \par  T.  Studer, ?A semantics for $\\lambda^\{ \\\{ \\\} \}_\{ \\mathsf \{str \}\}$: a calculus with overloading and late-binding?. Universit\'e4t Bern, 1999.\par \par  S.  Schwendimann, ?Aspects of Computational Logic?. Universit\'e4t Bern, 1998.\par \par  P.  Balsiger and A.  Heuerding, ?Comparison of Theorem Provers for Modal Logics ? Introduction and Summary?, in Proceedings of Tableaux '98, 1998, vol. 1397, p. 25\{?\}26.\par \par  R.  Kahle, ?Frege structures for partial applicative theories?, Journal of Logic and Computation, vol. 8, p. 683\{?\}700, 1998.\par \par  P.  Balsiger and A.  Heuerding, ?Logics Workbench 1.0?, in Proceedings of Tableaux '98, 1998, vol. 1397, p. 35\{?\}37.\par \par  S.  Schwendimann, ?A new one-pass tableau calculus for $\\mathsf\{PLTL\}$?, in Proceedings of Tableaux '98, 1998, vol. 1397, p. 277\{?\}292.\par \par  G.  J\'e4ger and R. F.  St\'e4rk, ?A proof-theoretic framework for logic programming?, in Handbook of Proof Theory, 1998, p. 639\{?\}682.\par \par  H.  Schlingloff and W.  Heinle, ?Relation Algebra and Modal Logics?, in Relational Methods in Computer Science, 1998, p. 20\{?\}89.\par \par  A.  Heuerding, ?Sequent Calculi for Proof Search in some Modal Logics?. Universit\'e4t Bern, 1998.\par \par  M.  Marzetta and T.  Strahm, ?The $?$ quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals?, Archive for Mathematical Logic, vol. 37, p. 391\{?\}413, 1998.\par \par  R.  Kahle, ?Applikative Theorien und Frege-Strukturen?. Universit\'e4t Bern, 1997.\par \par  T.  Studer, ?Explicit Mathematics: W-type, Models?. Universit\'e4t Bern, 1997.\par \par  E. E.  Clarke, M.  Fujita, and W.  Heinle, ?Hybrid spectral transform diagrams?. Carnegie Mellon University, 1997.\par \par  E. E.  Clarke, M.  Fujita, and W.  Heinle, ?Hybrid spectral transform diagrams?, in Proceedings of the International Conference on Information and Communications Security, 1997, vol. 1334, p. 251\{?\}255.\par \par  W.  Heinle and H.  Schlingloff, ?Modal rule correspondences?. Universit\'e4t Bern, 1997.\par \par  E. E.  Clarke, W.  Heinle, and H.  Schlingloff, ?Model checking?, in Handbook of Automated Reasoning, 1997, p. 1635\{?\}1790.\par \par  T.  Strahm, ?Polynomial time operations in explicit mathematics?, The Journal of Symbolic Logic, vol. 62, p. 575\{?\}594, 1997.\par \par  G.  J\'e4ger, ?Power types in explicit mathematics??, The Journal of Symbolic Logic, vol. 62, p. 1142\{?\}1146, 1997.\par \par  R.  Gor\'e9, W.  Heinle, and A.  Heuerding, ?Relations between propositional normal modal logics: an overview?, Journal of Logic and Computation, vol. 7, p. 649\{?\}658, 1997.\par \par  G.  J\'e4ger, ?Some proof theory of first order logic programming?, in Logic of Computation, 1997, vol. 157, p. 201\{?\}228.\par \par  R.  Kahle, ?Uniform limit in explicit mathematics with universes?. Universit\'e4t Bern, 1997.\par \par  A.  Heuerding and S.  Schwendimann, ?A benchmark method for the propositional modal logics K, KT, S4?. Universit\'e4t Bern, 1996.\par \par  A.  Heuerding, M.  Seyfried, and H.  Zimmermann, ?Efficient loop-check for backward proof search in some non-classical propositional logics?, in Proceedings of Tableaux '96, 1996, vol. 1071, p. 210\{?\}225.\par \par  R.  Kahle, ?Frege structures for partial applicative theories?. Universit\'e4t Bern, 1996.\par \par  A.  Heuerding, G.  J\'e4ger, S.  Schwendimann, and M.  Seyfried, ?A logics workbench?, The European Journal on Artificial Intelligence, vol. 9, p. 53\{?\}58, 1996.\par \par  A.  Heuerding, G.  J\'e4ger, S.  Schwendimann, and M.  Seyfried, ?The logics workbench LWB: a snapshot?, Euromath Bulletin, vol. 2, p. 177\{?\}186, 1996.\par \par  A.  Heuerding, ?LWBtheory: information about some propositional logics via the WWW?, Journal of the Interest Group in Pure and Applied Logic, vol. 4, p. 196\{?\}174, 1996.\par \par  A.  Heuerding and S.  Schwendimann, ?On the modal logic K plus theories?, in Proceedings of Computer Science Logic '95, 1996, vol. 1092, p. 308\{?\}319.\par \par  T.  Strahm, ?Partial applicative theories and explicit substitutions?, Journal of Logic and Computation, vol. 6, p. 55\{?\}77, 1996.\par \par  T.  Strahm, ?On the Proof Theory of Applicative Theories?. Universit\'e4t Bern, 1996.\par \par  G.  J\'e4ger and T.  Strahm, ?Some theories with positive induction of ordinal strength $\\varphi \\omega 0$?, The Journal of Symbolic Logic, vol. 61, p. 818\{?\}842, 1996.\par \par  T.  Glass and T.  Strahm, ?Systems of explicit mathematics with non-constructive $?$-operator and join?, Annals of Pure and Applied Logic, vol. 82, p. 193\{?\}219, 1996.\par \par  S.  Feferman and G.  J\'e4ger, ?Systems of explicit mathematics with non-constructive $?$-operator. Part II?, Annals of Pure and Applied Logic, vol. 79, p. 37\{?\}52, 1996.\par \par  R.  Kahle, ?Universes over Frege Structures?. Universit\'e4t Bern, 1996.\par \par  G.  J\'e4ger, ?A deductive approach to logic programming?, in Proof and Computation, 1995, vol. 139, p. 231\{?\}270.\par \par  A.  Heuerding, G.  J\'e4ger, S.  Schwendimann, and M.  Seyfried, ?LWB - a logics workbench, extended abstract?, in Proceedings of KI-95 Activities: Workshop, Posters, Demos, 1995, p. 73\{?\}74.\par \par  R.  Kahle, ?Natural numbers and forms of weak induction in applicative theories?. Universit\'e4t Bern, 1995.\par \par  A.  Heuerding, G.  J\'e4ger, S.  Schwendimann, and M.  Seyfried, ?Propositional logics on the computer?, in Proceedings of Theorem Proving with Analytic Tableaux and Related Methods, 1995, vol. 918, p. 310\{?\}323.\par \par  W.  Heinle and B. - H.  Schlingloff, ?Relational semantics for modal logics?, in Proceedings of Verification in New Orientations, 1995, pp. 104-131.\par \par  G.  J\'e4ger and T.  Strahm, ?Second order theories with ordinals and elementary comprehension?, Archive for Mathematical Logic, vol. 34, p. 345\{?\}375, 1995.\par \par  G.  J\'e4ger and T.  Strahm, ?Totality in applicative theories?, Annals of Pure and Applied Logic, vol. 74, p. 105\{?\}120, 1995.\par \par  B.  H\'f6sli and G.  J\'e4ger, ?About some symmetries of negation?, The Journal of Symbolic Logic, vol. 59, p. 473\{?\}485, 1994.\par \par  T.  Strassen, ?The basic logic of proofs?. University of Bern, 1994.\par \par  B.  B\'fctler, R.  Esser, G.  J\'e4ger, U. - M.  K\'fcnzi, H.  Lienhard, and R.  Mattmann, ?Executable models for analysis and implementation of complex systems?, in Proceedings of Information Conference of Swiss Priority Programme Informatics Research 1992\{?\}1996, Module 1: Secure Distributed Systems, 1994.\par \par  S.  Artemov and T.  Strassen, ?The Basic Logic of Proofs?, in \{C\}omputer \{S\}cience \{L\}ogic, 6th Workshop, \{CSL\}'92, \{S\}an \{M\}iniato, \{I\}taly, \{S\}eptember 28?\{O\}ctober 2, 1992, Selected Papers, 1993, vol. 702, pp. 14?28.\par \par  G.  J\'e4ger and R. F.  St\'e4rk, ?The defining power of stratified and hierarchical logic programs?, Journal of Logic Programming, vol. 15, p. 55\{?\}77, 1993.\par \par  G.  J\'e4ger, ?Fixed points in Peano arithmetic with ordinals?, Annals of Pure and Applied Logic, vol. 60, p. 119\{?\}132, 1993.\par \par  S.  Artemov and T.  Strassen, ?Functionality in the Basic Logic of Proofs?. Institut f\'fcr Informatik und angewandte Mathematik, 1993.\par \par  S.  Artemov and T.  Strassen, ?The Logic of the \{G\'f6del Proof Predicate?, in Computational Logic and Proof Theory, Third \{K\}urt \{G\'f6del \{C\}olloquium, \{KGC\}'93, \{B\}rno, \{C\}zech \{R\}epublic, \{A\}ugust 24?27, 1993, Proceedings, 1993, vol. 713, pp. 71?82.\par \par  G.  J\'e4ger, ?Some proof-theoretic aspects of logic programming?, in Logic and Algebra of Specification, 1993, vol. 94, p. 113\{?\}142.\par \par  S.  Feferman and G.  J\'e4ger, ?Systems of explicit mathematics with non-constructive $?$-operator. Part I?, Annals of Pure and Applied Logic, vol. 65, p. 243\{?\}263, 1993.\par \par  S.  Artemov and T.  Strassen, ?The Basic Logic of Proofs?. Institut f\'fcr Informatik und angewandte Mathematik, 1992.\par \par }