| [AF09a] | Luca Alberucci and Alessandro Facchini. The modal μ-calculus hierarchy over restricted classes of transition systems. Journal of Symbolic Logic, 74(4):1367--1400, 2009. [ bib | .pdf ] |
| [AF09b] | Luca Alberucci and Alessandro Facchini. On modal μ-calculus and Gödel-Löb logic. Studia Logica, 91:145--169, 2009. [ bib | .pdf ] |
| [AJ05] | Luca Alberucci and Gerhard Jäger. About cut elimination for logics of common knowledge. Annals of Pure and Applied Logic, 133(1--3):73--99, 2005. [ bib | DOI | .pdf ] |
| [AK09] | Sergei Artemov and Roman Kuznets. Logical omniscience as a computational complexity problem. In Aviad Heifetz, editor, Theoretical Aspects of Rationality and Knowledge, Proceedings of the Twelfth Conference (TARK 2009), pages 14--23, Stanford University, California, July 6--8, 2009. ACM. [ bib | DOI | .pdf ] |
| [AK14] | Sergei Artemov and Roman Kuznets. Logical Omniscience As Infeasibility. Annals of Pure and Applied Logic, 165(1):6--25, 2014. [ bib | DOI | .pdf ] |
| [AKS14] | Luca Alberucci, Jürg Krähenbühl, and Thomas Studer. Justifying induction on modal μ-formulae. Logic Journal of IGPL, 22:805--817, 2014. [ bib | DOI | arXiv | .pdf ] |
| [Alb02a] | Luca Alberucci. The Modal μ-Calculus and the Logic of Common Knowledge. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2002. [ bib | .pdf ] |
| [Alb02b] | Luca Alberucci. Strictness of the modal μ-calculus hierarchy. In Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors, Automata, Logics and infinite Games: A Guide to Current Research, volume 2500 of Lecture Notes in Computer Science, pages 185--201. Springer, 2002. [ bib | .ps ] |
| [Alb07] | Luca Alberucci. A syntactical treatment of simultaneous fixpoints in the modal μ-calculus. Technical report, Universität Bern, 2007. [ bib | .pdf ] |
| [Alb09] | Luca Alberucci. Sequent calculi for the modal μ-calculus over S5. Journal of Logic and Computation, 2009. Published online on January 22, 2009. [ bib | .pdf ] |
| [AS92] | Sergei Artemov and Tyko Strassen. The Basic Logic of Proofs. Technical Report iam--92--018, Institut für Informatik und angewandte Mathematik, 1992. [ bib | http ] |
| [AS93a] | Sergei Artemov and Tyko Strassen. The basic logic of proofs. In E. Börger, G. Jäger, H. Kleine Büning, S. Martini, and M. M. Richter, editors, Computer Science Logic, 6th Workshop, CSL'92, San Miniato, Italy, September 28--October 2, 1992, Selected Papers, volume 702 of Lecture Notes in Computer Science, pages 14--28. Springer, 1993. [ bib | DOI ] |
| [AS93b] | Sergei Artemov and Tyko Strassen. Functionality in the basic logic of proofs. Technical Report iam--93--004, Institut für Informatik und angewandte Mathematik, 1993. [ bib | http ] |
| [AS93c] | Sergei Artemov and Tyko Strassen. The logic of the Gödel proof predicate. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, Computational Logic and Proof Theory, Third Kurt Gödel Colloquium, KGC'93, Brno, Czech Republic, August 24--27, 1993, Proceedings, volume 713 of Lecture Notes in Computer Science, pages 71--82. Springer, 1993. [ bib | DOI ] |
| [AS04] | Luca Alberucci and Vincenzo Salipante. On modal μ-calculus and non-well-founded set theory. Journal of Philosophical Logic, 33(4):343--360, 2004. [ bib | .pdf ] |
| [Bal01] | Peter Balsiger. The MacLWB and the Logic of Likelihood. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2001. [ bib | .pdf ] |
| [BEJ+94] | B. Bütler, R. Esser, Gerhard Jäger, Urs-Martin Künzi, Heinz 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. [ bib ] |
| [BGK10] | Kai Brünnler, Remo Goetschi, and Roman Kuznets. A syntactic realization theorem for justification logics. In Lev Beklemishev, Valentin Goranko, and Valentin Shehtman, editors, Advances in Modal Logic, Volume 8, pages 39--58. College Publications, 2010. [ bib | .pdf ] |
| [BGS17] | Samuel Bucheli, Meghdad Ghari, and Thomas Studer. Temporal justification logic. In Sujata Ghosh and R. Ramanujam, editors, Proceedings of the Ninth Workshop on Methods for Modalities, Indian Institute of Technology, Kanpur, India, 8th to 10th January 2017, pages 59--74. Open Publishing Association, Open Publishing Association, 2017. [ bib | .pdf ] |
| [BH98a] | Peter Balsiger and Alain Heuerding. Comparison of theorem provers for modal logics -- introduction and summary. In Harrie C. M. de Swart, editor, Proceedings of Tableaux '98, volume 1397 of Lecture Notes in Computer Science, pages 25--26. Springer, 1998. [ bib ] |
| [BH98b] | Peter Balsiger and Alain Heuerding. Logics Workbench 1.0. In Harrie C. M. de Swart, editor, Proceedings of Tableaux '98, volume 1397 of Lecture Notes in Computer Science, pages 35--37. Springer, 1998. [ bib ] |
| [BHS00] | Peter Balsiger, Alain Heuerding, and Stefan Schwendimann. A benchmark method for the propositional modal logics K, KT, S4. Journal of Automated Reasoning, 24(3):297--317, 2000. [ bib | .pdf ] |
| [BJS16] | Ulrik Torben Buchholtz, Gerhard Jäger, and Thomas Adrian Strahm. Theories of proof-theoretic strength ψ(Γ?+1). In Dieter Probst and Peter Schuster, editors, Concepts of Proof in Mathematics, Philosophy, and ComputerScience, volume 6 of Ontos Mathematical Logic. De Gruyter, January 2016. [ bib | .pdf ] |
| [BK09] | Samuel R. Buss and Roman Kuznets. The NP-completeness of reflected fragments of justification logics. In Sergei Artemov and Anil Nerode, editors, Proceedings of Symposium on Logical Foundations of Computer Science (LFCS'09), volume 5407 of Lecture Notes in Computer Science, pages 122--136, 2009. [ bib | DOI | .pdf ] |
| [BK12] | Samuel R. Buss and Roman Kuznets. Lower complexity bounds in justification logic. Annals of Pure and Applied Logic, 163(7):888--905, July 2012. Published online November 2011. [ bib | DOI | http | .pdf ] |
| [BKR+10] | Samuel Bucheli, Roman Kuznets, Bryan Renne, Joshua Sack, and Thomas Studer. Justified Belief Change. In Xabier Arrazola and María Ponte, editors, Proceedings of the Second ILCLI International Workshop on Logic and Philosphy of Knowledge, Communication and Action (LogKCA-10), pages 135--155. University of the Basque Country Press, November 2010. [ bib | .pdf ] |
| [BKS10a] | Samuel Bucheli, Roman Kuznets, and Thomas Studer. Explicit evidence systems with common knowledge. E-print 1005.0484, arXiv.org, May 2010. [ bib | http ] |
| [BKS10b] | Samuel Bucheli, Roman Kuznets, and Thomas Studer. Two ways to common knowledge. In Thomas Bolander and Torben Braüner, editors, Proceedings of the 6th Workshop on Methods for Modalities (M4M--6 2009), Copenhagen, Denmark, 12--14 November 2009, number 262 in Electronic Notes in Theoretical Computer Science, pages 83--98. Elsevier, May 2010. [ bib | DOI | .pdf ] |
| [BKS11a] | Samuel Bucheli, Roman Kuznets, and Thomas Studer. Justifications for common knowledge. Journal of Applied Non-classical Logics, 21(1):35--60, 2011. [ bib | DOI | .pdf ] |
| [BKS11b] | Samuel Bucheli, Roman Kuznets, and Thomas Studer. Partial Realization in Dynamic Justification Logic. In Lev D. Beklemishev and Ruy de Queiroz, editors, Logic, Language, Information and Computation, 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, 2011, Proceedings, volume 6642 of Lecture Notes in Artificial Intelligence, pages 35--51, 2011. [ bib | DOI | .pdf ] |
| [BKS13] | Samuel Bucheli, Roman Kuznets, and Thomas Studer. Decidability for Justification Logics Revisited. In Guram Bezhanishvili, Sebastian Löbner, Vincenzo Marra, and Frank Richter, editors, Logic, Language, and Computation, 9th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2011, Kutaisi, Georgia, September 26-30, 2011, Revised Selected Papers, volume 7758 of LNCS, pages 166--181. Springer, 2013. [ bib | DOI | .pdf ] |
| [BKS14] | Samuel Bucheli, Roman Kuznets, and Thomas Studer. Realizing Public Announcements by Justifications. Journal of Computer and System Sciences, 80(6):1046--1066, 2014. [ bib | DOI | .pdf ] |
| [BL05] | Kai Brünnler and Stéphane Lengrand. On two forms of bureaucracy in derivations. In Paola Bruscoli, François Lamarche, and Charles Stewart, editors, Proceedings of Structures and Deduction, pages 65--74. Technische Universität Dresden, 2005. [ bib | .pdf ] |
| [BL08] | Kai Brünnler and Martin Lange. Cut-free sequent systems for temporal logic. Journal of Logic and Algebraic Programming, 76(2):216--225, 2008. [ bib | DOI | .pdf ] |
| [BM08] | Kai Brünnler and Richard McKinley. An algorithmic interpretation of a deep inference system. In I. Cervesato, H. Veith, and A. Voronkov, editors, LPAR 2008, volume 5330 of Lecture Notes in Computer Science, pages 482---496. Springer-Verlag, 2008. [ bib | .pdf ] |
| [Bor99] | Afshin D. Boroumand. Logics workbench für window system. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1999. [ bib ] |
| [BPS08] | Kai Brünnler, Dieter Probst, and Thomas Studer. On contraction and the modal fragment. Mathematical Logic Quarterly, 54(4):345--349, 2008. [ bib | .pdf ] |
| [Bra13] | Peppo Brambilla. Proof Search in Propositional Circumscription and Default Logic. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2013. [ bib | .pdf ] |
| [Bri99] | Jimmy Brignioni. Konstruktion von Gegenmodellen intuitionistisch unbeweisbarer Sequenzen. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1999. [ bib ] |
| [Brü06a] | Kai Brünnler. Cut elimination inside a deep inference system for classical predicate logic. Studia Logica, 82(1):51--71, 2006. [ bib | DOI | .pdf ] |
| [Brü06b] | Kai Brünnler. Deep inference and its normal form of derivations. In Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker, editors, Proceedings of Computability in Europe, volume 3988 of Lecture Notes in Computer Science, pages 65--74. Springer, 2006. [ bib | DOI | .pdf ] |
| [Brü06c] | Kai Brünnler. Deep sequent systems for modal logic. In Guido Governatori, Ian Hodkinson, and Yde Venema, editors, Proceedings of Advances in Modal Logic, volume 6, pages 107--119. College Publications, 2006. [ bib | .pdf ] |
| [Brü06d] | Kai Brünnler. Locality for classical logic. Notre Dame Journal of Formal Logic, 47(4):557--580, 2006. [ bib | DOI | .pdf ] |
| [Brü09] | Kai Brünnler. Deep sequent systems for modal logic. Archive for Mathematical Logic, 48:551--577, 2009. [ bib | DOI | .pdf ] |
| [Bru10a] | Jon Brugger. Proof-theoretic aspects of weak König's Lemma. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2010. [ bib | .pdf ] |
| [Brü10b] | Kai Brünnler. Nested Sequents. Habilitationsschrift, Universität Bern, Institut für Informatik und angewandte Mathematik, 2010. [ bib | http ] |
| [BS09a] | Kai Brünnler and Lutz Straßburger. Modular sequent systems for modal logic. In Martin Giese and Arild Waaler, editors, Tableaux 2009, volume 5607 of Lecture Notes in Computer Science. Springer-Verlag, 2009. [ bib | DOI | .pdf ] |
| [BS09b] | Kai Brünnler and Thomas Studer. Syntactic cut-elimination for common knowledge. In C. Areces and S. Demri, editors, Proceedings of Methods for Modalities M4M5, volume 231 of ENTCS, pages 227--240. Elsevier, 2009. [ bib | DOI | .pdf ] |
| [BS09c] | Kai Brünnler and Thomas Studer. Syntactic cut-elimination for common knowledge. Annals of Pure and Applied Logic, 160(1):82--95, 2009. [ bib | DOI | .pdf ] |
| [BS12] | Kai Brünnler and Thomas Studer. Syntactic cut-elimination for a fragment of the modal mu-calculus. Annals of Pure and Applied Logic, 163(12):1838--1853, 2012. [ bib | .pdf ] |
| [BS17] | S. Berardi and Silvia Steila. Ramsey's theorem for pairs and k colors as a sub-classical principle of arithmetic. Journal of Symbolic Logic, 82:737--753, 2017. [ bib | .pdf ] |
| [Buc99] | Irene Bucher. Extension of the modal system KT4. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1999. [ bib ] |
| [Buc08] | Samuel Bucheli. Explicit mathematics with positive existential stratified comprehension, join and uniform monotone inductive definitions. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2008. [ bib | .pdf ] |
| [Buc12] | Samuel Bucheli. Justification Logics with Common Knowledge. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2012. [ bib | .pdf ] |
| [Bur04] | Theo Burri. Weak könig's lemma and extensional equality. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2004. [ bib | .pdf ] |
| [CFH97a] | Edmund M. Clarke, Masayuki Fujita, and Wolfgang Heinle. Hybrid spectral transform diagrams. Technical Report CMU--CS--97--149, Carnegie Mellon University, Department of Computer Science, 1997. [ bib ] |
| [CFH97b] | Edmund M. Clarke, Masayuki Fujita, and Wolfgang Heinle. Hybrid spectral transform diagrams. In Yongfei Han, Tatsuaki Okamoto, and Sihan Qing, editors, Proceedings of the International Conference on Information and Communications Security, volume 1334 of Lecture Notes in Computer Science, pages 251--255. Springer, 1997. [ bib ] |
| [CHS97] | Edmund M. Clarke, Wolfgang Heinle, and Holger Schlingloff. Model checking. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 1635--1790. Elsevier Science, 1997. [ bib ] |
| [DS05] | Michael Dürig and Thomas Studer. Probabilistic ABox reasoning: preliminary results. In Ian Horrocks, Ulrike Sattler, and Frank Wolter, editors, Proceedings of Description Logics '05, volume 147 of CEUR Workshop Proceedings, pages 104--111. CEUR-WS.org, 2005. [ bib | .pdf ] |
| [Dür05] | Michael Dürig. PALC: Extending ALC ABoxes with probabilities. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2005. [ bib | .pdf ] |
| [Ebe09] | Sebastian Eberhard. Aspekte beweisbar totaler Funktionen in applikativen Theorien. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2009. [ bib | .pdf ] |
| [Ebe13] | Sebastian Eberhard. Weak applicative theories, truth, and computational complexity. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2013. [ bib | .pdf ] |
| [Ebe14] | Sebastian Eberhard. A feasible theory of truth over combinatory algebra. Annals of Pure and Applied Logic, 165(5):1009--1033, 2014. [ bib | DOI | .pdf ] |
| [Ebe15] | Sebastian Eberhard. Applicative theories for logarithmic complexity classes. Theoretical Computer Science, 585:115--135, June 2015. [ bib | .pdf ] |
| [ES12] | Sebastian Eberhard and Thomas Strahm. Weak theories of truth and explicit mathematics. In Ulrich Berger, Hannes Diener, Peter Schuster, and Monika Seisenberger, editors, Logic, Construction, Computation, pages 157--184. Ontos Verlag, 2012. [ bib | .pdf ] |
| [ES15] | Sebastian Eberhard and Thomas Adrian Strahm. Unfolding feasible arithmetic and weak truth. In Theodora Achourioti, Henri Galinon, José Martínez Fernández, and Kentaro Fujimoto, editors, Unifying the Philosophy of Truth, volume 36 of Logic, Epistemology, and the Unity of Science, pages 153--167. Springer Netherlands, Dordrecht, 2015. [ bib | .pdf ] |
| [Fab11] | Daniel Fabian. Applicative theories on tree ordinal numbers. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2011. [ bib | .pdf ] |
| [FJ93] | Solomon Feferman and Gerhard Jäger. Systems of explicit mathematics with non-constructive μ-operator. Part I. Annals of Pure and Applied Logic, 65(3):243--263, 1993. [ bib | .pdf ] |
| [FJ96] | Solomon Feferman and Gerhard Jäger. Systems of explicit mathematics with non-constructive μ-operator. Part II. Annals of Pure and Applied Logic, 79(1):37--52, 1996. [ bib | DOI | http ] |
| [FK15] | Melvin Fitting and Roman Kuznets. Modal interpolation via nested sequents. Annals of pure and applied logic, 166(3):274--305, March 2015. [ bib | .pdf ] |
| [Flu13] | Dandolo Flumini. Weak well orders. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2013. [ bib | .pdf ] |
| [FS00] | Solomon Feferman and Thomas Strahm. The unfolding of non-finitist arithmetic. Annals of Pure and Applied Logic, 104(1--3):75--96, 2000. [ bib | .ps ] |
| [FS10] | Solomon Feferman and Thomas Strahm. Unfolding finitist arithmetic. Review of Symbolic Logic, 3(4):665--689, 2010. [ bib | .pdf ] |
| [FS14] | Dandolo Flumini and Kentaro Sato. From hierarchies to well-foundedness. Archive for Mathematical Logic, 53(7--8), 2014. [ bib | DOI | .pdf ] |
| [FSY17] | Emanuele Frittaion, Silvia Steila, and Keita Yokoyama. The strength of the sct criterion. In T. V. Gopal, Gerhard Jäger, and Silvia Steila, editors, Theory and Applications of Models of Computation - 14th Annual Conference, TAMC 2017, Bern, Switzerland, April 20-22, 2017, Proceedings, page 260273, 2017. [ bib | DOI | .pdf ] |
| [GHH97] | Rajeev Goré, Wolfgang Heinle, and Alain Heuerding. Relations between propositional normal modal logics: an overview. Journal of Logic and Computation, 7(5):649--658, 1997. [ bib | .ps ] |
| [GK12] | Remo Goetschi and Roman Kuznets. Realization for Justification Logics via Nested Sequents: Modularity through Embedding. Annals of Pure and Applied Logic, 163(9):1271--1298, September 2012. [ bib | DOI | http | .pdf ] |
| [Goe08] | Remo Goetschi. Polytime functions in two-sorted bounded arithmetic. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2008. [ bib | .pdf ] |
| [Goe12] | Remo Goetschi. On the Realization and Classification of Justification Logics. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2012. [ bib | .pdf ] |
| [GS96] | Thomas Glass and Thomas Strahm. Systems of explicit mathematics with non-constructive μ-operator and join. Annals of Pure and Applied Logic, 82(2):193--219, 1996. [ bib | .ps ] |
| [Hei01] | Marc Heissenbüttel. Theories of ordinal strength φ2 0 and φ2 ε0. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2001. [ bib | .pdf ] |
| [Heu96] | Alain Heuerding. LWBtheory: information about some propositional logics via the WWW. Journal of the Interest Group in Pure and Applied Logic, 4(4):196--174, 1996. [ bib | .ps ] |
| [Heu98] | Alain Heuerding. Sequent Calculi for Proof Search in some Modal Logics. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1998. [ bib | .pdf ] |
| [HJ94] | Brigitte Hösli and Gerhard Jäger. About some symmetries of negation. The Journal of Symbolic Logic, 59(2):473--485, 1994. [ bib | http ] |
| [HJSS95a] | Alain Heuerding, Gerhard Jäger, Stefan Schwendimann, and Michael Seyfried. LWB - a logics workbench, extended abstract. In L. Dreschler-Fischer and S. Pribbenow, editors, Proceedings of KI-95 Activities: Workshop, Posters, Demos, pages 73--74. Gesellschaft für Informatik, 1995. [ bib ] |
| [HJSS95b] | Alain Heuerding, Gerhard Jäger, Stefan Schwendimann, and Michael Seyfried. Propositional logics on the computer. In Peter Baumgartner, Reiner Hähnle, and Joachim Posegga, editors, Proceedings of Theorem Proving with Analytic Tableaux and Related Methods, volume 918 of Lecture Notes in Computer Science, pages 310--323. Springer, 1995. [ bib | .ps ] |
| [HJSS96a] | Alain Heuerding, Gerhard Jäger, Stefan Schwendimann, and Michael Seyfried. A logics workbench. The European Journal on Artificial Intelligence, 9(2):53--58, 1996. [ bib ] |
| [HJSS96b] | Alain Heuerding, Gerhard Jäger, Stefan Schwendimann, and Michael Seyfried. The logics workbench LWB: a snapshot. Euromath Bulletin, 2(1):177--186, 1996. [ bib | .ps ] |
| [HS95] | Wolfgang Heinle and Bernd-Holger Schlingloff. Relational semantics for modal logics. In Robert Rodosek, editor, Proceedings of Verification in New Orientations, pages 104--131. University of Maribor, 1995. [ bib | .ps ] |
| [HS96a] | Alain Heuerding and Stefan Schwendimann. A benchmark method for the propositional modal logics K, KT, S4. Technical Report IAM--96--015, Universität Bern, Institut für Informatik und angewandte Mathematik, 1996. [ bib | .ps ] |
| [HS96b] | Alain Heuerding and Stefan Schwendimann. On the modal logic K plus theories. In Hans Kleine Büning, editor, Proceedings of Computer Science Logic '95, volume 1092 of Lecture Notes in Computer Science, pages 308--319. Springer, 1996. [ bib | .ps ] |
| [HS97] | Wolfgang Heinle and Holger Schlingloff. Modal rule correspondences. Dagstuhl Seminar report 9403, Universität Bern, 1997. [ bib ] |
| [HSZ96] | Alain Heuerding, Michael Seyfried, and Heinrich Zimmermann. Efficient loop-check for backward proof search in some non-classical propositional logics. In Pierangelo Miglioli, Ugo Moscato, Daniele Mundici, and Mario Ornaghi, editors, Proceedings of Tableaux '96, volume 1071 of Lecture Notes in Computer Science, pages 210--225. Springer, 1996. [ bib | .ps ] |
| [Jäg93a] | Gerhard Jäger. Fixed points in Peano arithmetic with ordinals. Annals of Pure and Applied Logic, 60(2):119--132, 1993. [ bib | DOI | http ] |
| [Jäg93b] | Gerhard Jäger. Some proof-theoretic aspects of logic programming. In Friedrich Ludwig Bauer, Wilfried Brauer, and Helmut Schwichtenberg, editors, Logic and Algebra of Specification, volume 94 of Computer and Systems Sciences, pages 113--142. Springer, 1993. [ bib ] |
| [Jäg95] | Gerhard Jäger. A deductive approach to logic programming. In Helmut Schwichtenberg, editor, Proof and Computation, volume 139 of NATO ASI Series F, pages 231--270. Springer, 1995. [ bib ] |
| [Jäg97a] | Gerhard Jäger. Power types in explicit mathematics? The Journal of Symbolic Logic, 62(4):1142--1146, 1997. [ bib | http ] |
| [Jäg97b] | Gerhard Jäger. Some proof theory of first order logic programming. In Helmut Schwichtenberg, editor, Logic of Computation, volume 157 of NATO Science Series, pages 201--228. Springer, 1997. [ bib ] |
| [Jäg01] | Gerhard Jäger. First order theories for nonmonotone inductive definitions: recursively inaccessible and Mahlo. The Journal of Symbolic Logic, 66(3):1073--1089, 2001. [ bib | .pdf ] |
| [Jäg04] | Gerhard Jäger. An intensional fixed point theory over first order arithmetic. Annals of Pure and Applied Logic, 128(1--3):197--213, 2004. [ bib | .pdf ] |
| [Jäg05] | Gerhard Jäger. Metapredicative and explicit Mahlo: a proof-theoretic perspective. In Rene Cori, Alexander Razborov, Stevo Todorcevic, and Carol Wood, editors, Proceedings of Logic Colloquium '00, volume 19 of Association of Symbolic Logic Lecture Notes in Logic, pages 272--293. AK Peters, 2005. [ bib | .pdf ] |
| [Jäg07] | Gerhard Jäger. On Feferman's operational set theory OST. Annals of Pure and Applied Logic, 150(1--3):19--39, 2007. [ bib | .pdf ] |
| [Jäg09a] | Gerhard Jäger. Full operational set theory with unbounded existential quantification and power set. Annals of Pure and Applied Logic, 160(1):33--52, July 2009. [ bib | .pdf ] |
| [Jäg09b] | Gerhard Jäger. Operations, sets and classes. In C. Glymour, W. Wei, and D. Westerstahl, editors, Logic, Methodology and Philosophy of Science - Proceedings of the Thirteenth International Congress. College Publications, 2009. [ bib | .pdf ] |
| [Jäg10] | Gerhard Jäger. Modal Fixed Point Logics. In J. Esparza, B. Spanfelner, and O. Grumberg, editors, Logics and Languages for Reliability and Security, volume 25 of NATO Science for Peace and Security Series - D: Information and Communication Security. IOS Press, 2010. [ bib | DOI | .pdf ] |
| [Jäg13] | Gerhard Jäger. Operational closure and stability. Annals of Pure and Applied Logic, 164(7–8):813 -- 821, 2013. [ bib | DOI | .pdf ] |
| [Jäg16] | Gerhard Jäger. Relativizing operational set theory. The Bulletin of Symbolic Logic, 2016. [ bib | .pdf ] |
| [Jäg18] | Gerhard Jäger. The Operational Penumbra: Some Ontological Aspects, volume 13. Springer International Publishing, 2018. [ bib | .pdf ] |
| [JK10] | Gerhard Jäger and Jürg Krähenbühl. Σ11 choice in a theory of sets and classes. In Ralf Schindler, editor, Ways of Proof Theory, pages 283--314. Ontos Verlag, 2010. [ bib | .pdf ] |
| [JKS99] | Gerhard Jäger, Reinhard Kahle, and Thomas Strahm. On applicative theories. In Andrea Cantini, Ettore Casari, and Pierluigi Minari, editors, Logic and Foundations of Mathematics, pages 83--92. Kluwer, 1999. [ bib | .ps ] |
| [JKS01] | Gerhard Jäger, Reinhard Kahle, and Thomas Studer. Universes in explicit mathematics. Annals of Pure and Applied Logic, 109(3):141--162, 2001. [ bib | .pdf ] |
| [JKS05] | Gerhard Jäger, Mathis Kretz, and Thomas Studer. Cut-free axiomatizations for stratified modal fixed point logic. In Holger Schlingloff, editor, Proceedings of Methods for Modalities 4, volume 194 of Humboldt-Universität Berlin Informatik-Berichte, pages 125--143. Humboldt-Universität Berlin, 2005. [ bib | .pdf ] |
| [JKS07] | Gerhard Jäger, Mathis Kretz, and Thomas Studer. Cut-free common knowledge. Journal of Applied Logic, 5(4):681--689, 2007. [ bib | DOI | .pdf ] |
| [JKS08] | Gerhard Jäger, Mathis Kretz, and Thomas Studer. Canonical completeness of infinitary mu. Journal of Logic and Algebraic Programming, 76(2):270--292, 2008. [ bib | DOI | .pdf ] |
| [JKSS99] | Gerhard Jäger, Reinhard Kahle, Anton Setzer, and Thomas Strahm. The proof-theoretic analysis of transfinitely iterated fixed point theories. The Journal of Symbolic Logic, 64(1):53--67, 1999. [ bib | .ps ] |
| [JM16a] | Gerhard Jäger and Michel Marti. A canonical model construction for intuitionistic distributed knowledge. In Advances in Modal Logic 2016. College Publications, College Publications, 2016. [ bib | .pdf ] |
| [JM16b] | Gerhard Jäger and Michel Marti. Intuitionistic common knowledge or belief. Journal of applied logic, 2016. [ bib | .pdf ] |
| [JP04a] | Gerhard Jäger and Dieter Probst. Iterating Σ operations in admissible set theory without foundation: a further aspect of metapredicative Mahlo. In Godehart Link, editor, One Hundred Years of Russell's Paradox. Papers from the 2001 Munich Russell Conference, pages 119--134. de Gruyter, 2004. [ bib | .pdf ] |
| [JP04b] | Gerhard Jäger and Dieter Probst. Variation on a theme of Schütte. Mathematical Logic Quarterly, 50(3):258--264, 2004. [ bib | .pdf ] |
| [JP11] | Gerhard Jäger and Dieter Probst. The suslin operator in applicative theories: Its proof-theoretic analysis via ordinal theories. Annals of Pure and Applied Logic, 162(8):647--660, 2011. [ bib | DOI | .pdf ] |
| [JS93] | Gerhard Jäger and Robert F. Stärk. The defining power of stratified and hierarchical logic programs. Journal of Logic Programming, 15(1--2):55--77, 1993. [ bib | .pdf ] |
| [JS95a] | Gerhard Jäger and Thomas Strahm. Second order theories with ordinals and elementary comprehension. Archive for Mathematical Logic, 34(6):345--375, 1995. [ bib | .ps ] |
| [JS95b] | Gerhard Jäger and Thomas Strahm. Totality in applicative theories. Annals of Pure and Applied Logic, 74(2):105--120, 1995. [ bib | .ps ] |
| [JS96] | Gerhard Jäger and Thomas Strahm. Some theories with positive induction of ordinal strength φ ω0. The Journal of Symbolic Logic, 61(3):818--842, 1996. [ bib | .ps ] |
| [JS98] | Gerhard Jäger and Robert F. Stärk. A proof-theoretic framework for logic programming. In Samuel S. Buss, editor, Handbook of Proof Theory, pages 639--682. North-Holland, 1998. [ bib | DOI | http ] |
| [JS99] | Gerhard Jäger and Thomas Strahm. Bar induction and ω model reflection. Annals of Pure and Applied Logic, 97(1--3):221--230, 1999. [ bib | .ps ] |
| [JS00] | Gerhard Jäger and Thomas Strahm. Fixed point theories and dependent choice. Archive for Mathematical Logic, 39(7):493--508, 2000. [ bib | .ps ] |
| [JS01] | Gerhard Jäger and Thomas Strahm. Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory. The Journal of Symbolic Logic, 66(2):935--958, 2001. [ bib | .pdf ] |
| [JS02a] | Gerhard Jäger and Thomas Strahm. The proof-theoretic analysis of the Suslin operator in applicative theories. In Wilfried Sieg, Richard Sommer, and Carolyn Talcott, editors, Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, pages 270--292. AK Peters, 2002. [ bib | .pdf ] |
| [JS02b] | Gerhard Jäger and Thomas Studer. Extending the system T0 of explicit mathematics: the limit and Mahlo axioms. Annals of Pure and Applied Logic, 114(1--3):79--101, 2002. [ bib | .pdf ] |
| [JS05] | Gerhard Jäger and Thomas Strahm. Reflections on reflections in explicit mathematics. Annals of Pure and Applied Logic, 136(1--2):116--133, 2005. [ bib | .pdf ] |
| [JS11] | Gerhard Jäger and Thomas Studer. A Buchholz rule for modal fixed point logics. Logica Universalis, 5(1):1--19, 2011. [ bib | DOI | .pdf ] |
| [JZ12] | Gerhard Jäger and Rico Zumbrunnen. About the Strength of Operational Regularity. In Ulrich Berger, Hannes Diener, Peter Schuster, and Monika Seisenberger, editors, Logic, Construction, Computation, pages 305--324. Ontos Verlag, 2012. [ bib | .pdf ] |
| [JZ14] | Gerhard Jäger and Rico Zumbrunnen. Explicit mathematics and operational set theory: some ontological comparisons. The Bulletin of Symbolic Logic, 20:275--292, September 2014. [ bib | DOI | .pdf ] |
| [Kah95] | Reinhard Kahle. Natural numbers and forms of weak induction in applicative theories. Technical Report IAM--95--001, Universität Bern, Institut für Informatik und angewandte Mathematik, 1995. [ bib | .ps ] |
| [Kah96a] | Reinhard Kahle. Frege structures for partial applicative theories. Technical Report IAM--96--013, Universität Bern, Institut für Informatik und angewandte Mathematik, 1996. [ bib ] |
| [Kah96b] | Reinhard Kahle. Universes over Frege structures. Technical Report IAM--96--010, Universität Bern, Institut für Informatik und angewandte Mathematik, 1996. [ bib | .ps ] |
| [Kah97a] | Reinhard Kahle. Applikative Theorien und Frege-Strukturen. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1997. [ bib | .ps ] |
| [Kah97b] | Reinhard Kahle. Uniform limit in explicit mathematics with universes. Technical Report IAM--97--002, Universität Bern, Institut für Informatik und angewandte Mathematik, 1997. [ bib | .ps ] |
| [Kah98] | Reinhard Kahle. Frege structures for partial applicative theories. Journal of Logic and Computation, 8(5):683--700, 1998. [ bib | DOI | http ] |
| [Kah00] | Reinhard Kahle. N-strictness in applicative theories. Archive for Mathematical Logic, 39(2):125--144, 2000. [ bib | DOI | http ] |
| [Kel02] | Philipp Keller. Information flow -- logics for the (r)age of information. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2002. [ bib | .pdf ] |
| [KMOS15] | Ioannis Kokkinis, Petar Maksimović, Zoran Ognjanović, and Thomas Studer. First steps towards probabilistic justification logic. Logic Journal of IGPL, 23(4):662--687, June 2015. [ bib | .pdf ] |
| [Koh12] | Roger Peter Kohler. Java-Programm zur interaktiven Bearbeitung von JALC-Herleitungen. Bachelor's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2012. [ bib | .pdf ] |
| [Kok16a] | Ioannis Kokkinis. The complexity of non-iterated probabilistic justification logic. In Marc Gyssens and Guillermo Ricardo Simari, editors, Foundations of Information and Knowledge Systems - 9th International Symposium, FoIKS 2016, Linz, Austria, March 7-11, 2016. Proceedings, volume 9616 of Lecture Notes in Computer Science, pages 292--310. Springer, 2016. [ bib | .pdf ] |
| [Kok16b] | Ioannis Kokkinis. Uncertain Reasoning in Justification Logic. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2016. [ bib | .pdf ] |
| [KOS16] | Ioannis Kokkinis, Zoran Ognjanović, and Thomas Studer. Probabilistic justification logic. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science - International Symposium, LFCS 2016, Deerfield Beach, FL, USA, January 4-7, 2016. Proceedings, volume 9537 of Lecture Notes in Computer Science, pages 174--186. Springer, 2016. [ bib | .pdf ] |
| [Kot06] | Norbert Kottmann. Description logic query answering with relational databases. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2006. [ bib | .pdf ] |
| [Krä06] | Jürg Krähenbühl. Explicit mathematics with positive existential comprehension and join. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2006. [ bib | .pdf ] |
| [Krä09] | Jürg Krähenbühl. Justifying induction on modal mu-formulae. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2009. [ bib | .pdf ] |
| [Krä11] | Jürg Krähenbühl. On the Relationship between Choice Schemes and Iterated Class Comprehension in Set Theory. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2011. [ bib | .pdf ] |
| [Kre00] | Michel Krebs. Einige Aspekte der Modallogik S5n mit Allgemeinwissen. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2000. [ bib | .pdf ] |
| [Kre02] | Mathis Kretz. On the treatment of predicative polymorphism in theories of explicit mathematics. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2002. [ bib | .pdf ] |
| [Kre06] | Mathis Kretz. Proof-Theoretic Aspects of Modal Logic with Fixed Points. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2006. [ bib | .pdf ] |
| [KS00] | Reinhard Kahle and Thomas Studer. A theory of explicit mathematics equivalent to ID1. In Peter Clote and Helmut Schwichtenberg, editors, Proceedings of Computer Science Logic, volume 1862 of Lecture Notes in Computer Science, pages 356--370. Springer, 2000. [ bib | .pdf ] |
| [KS01] | Reinhard Kahle and Thomas Studer. Formalizing non-termination of recursive programs. Journal of Logic and Algebraic Programming, 49(1--2):1--14, 2001. [ bib | .pdf ] |
| [KS06] | Mathis Kretz and Thomas Studer. Deduction chains for common knowledge. Journal of Applied Logic, 4(3):331--357, 2006. [ bib | DOI | .pdf ] |
| [KS07] | Norbert Kottmann and Thomas Studer. Improving semantic query answering. In Roland Wagner, Norman Revell, and Günther Pernul, editors, Proceedings of Database and Expert Systems Applications, volume 4653 of Lecture Notes in Computer Science, pages 671--679. Springer, 2007. [ bib | .pdf ] |
| [KS12] | Roman Kuznets and Thomas Studer. Justifications, Ontology, and Conservativity. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence Moss, editors, Advances in Modal Logic, volume 9, pages 437--458. College Publications, 2012. [ bib | .pdf ] |
| [KS13] | Roman Kuznets and Thomas Studer. Update as Evidence: Belief Expansion. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2013, San Diego, CA, USA, January 6--8, 2013, Proceedings, volume 7734 of Lecture Notes in Computer Science, pages 266--279. Springer, 2013. [ bib | DOI | .pdf ] |
| [KS16a] | Ioannis Kokkinis and Thomas Studer. Cyclic proofs for linear temporal logic. In Dieter Probst and Peter Schuster, editors, Concepts of Proof in Mathematics, Philosophy, and Computer Science, volume 6 of Ontos Mathematical Logic. De Gruyter, 2016. [ bib | .pdf ] |
| [KS16b] | Roman Kuznets and Thomas Studer. Weak arithmetical interpretations for the logic of proofs. Logic Journal of IGPL, 24(3):424--440, 2016. [ bib | .pdf ] |
| [KSS16] | Reinhard Kahle, Thomas Strahm, and Thomas Studer, editors. Advances in Proof Theory, volume 28 of Progress in Computer Science and Applied Logic. Springer International Publishing, 2016. [ bib ] |
| [Kuz09] | Roman Kuznets. A note on the use of sum in the Logic of Proofs. In Costas Drossos, Pavlos Peppas, and Constantine Tsinakis, editors, Proceedings of the 7th Panhellenic Logic Symposium, pages 99--103, Patras University, Greece, July 15--19, 2009. Patras University Press. [ bib | .pdf ] |
| [Kuz10] | Roman Kuznets. Self-referential justifications in epistemic logic. Theory of Computing Systems, 46(4):636--661, May 2010. [ bib | DOI | .pdf ] |
| [Lar08] | Ciro Larrzabal. Automatic Model Checking of UML models. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2008. [ bib | .pdf ] |
| [Lin08] | Simone Liniger. The Basic Feasible Functionals in Bounded Arithmetic. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2008. [ bib | .pdf ] |
| [Mar17] | Michel Marti. Contributions to Intuitionistic Epistemic Logic. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2017. [ bib | .pdf ] |
| [McK08] | Richard McKinley. Soft linear set theory. Journal of Logic and Algebraic Programming, 76(2):226--245, 2008. [ bib | .pdf ] |
| [McK10] | Richard McKinley. Expansion nets: Proof nets for for propositional classical logic. In Christian Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 17), volume 6397 of Lecture Notes in Computer Science, pages 535--549. Springer Berlin / Heidelberg, 2010. 10.1007/978-3-642-16242-8_38. [ bib | .pdf ] |
| [McK13a] | Richard McKinley. Canonical proof nets for classical logic. Annals of Pure and Applied Logic, 164(6):702--732, 2013. [ bib | DOI | .pdf ] |
| [McK13b] | Richard McKinley. Proof nets for Herbrand's Theorem. ACM Transactions on Computational Logic, 14(1):5, 2013. [ bib | DOI | .pdf ] |
| [MM14] | Michel Marti and George Metcalfe. A Hennessy-Milner Property for Many-Valued Modal Logics. In Rajeev Goré and Barteld Kooi and and Agi Kurucz, editor, Advances in Modal Logic, volume 10, pages 407--420. College Publications, 2014. [ bib | .pdf ] |
| [MS98] | Markus Marzetta and Thomas Strahm. The μ quantification operator in explicit mathematics with universes and iterated fixed point theories with ordinals. Archive for Mathematical Logic, 37(5):391--413, 1998. [ bib | .ps ] |
| [MS12] | Grigori Mints and Thomas Studer. Cut-elimination for the mu-calculus with one variable. In Fixed Points in Computer Science 2012, volume 77 of EPTCS, pages 47--54. Open Publishing Association, 2012. [ bib | .pdf ] |
| [MS16] | Michel Marti and Thomas Studer. Intuitionistic modal logic made explicit. IfCoLog Journal of Logics and their Applications, 3(5):877--901, 2016. [ bib | .pdf ] |
| [MT99] | Grigori Mints and Sergei Tupailo. Epsilon-substitution method for the ramified language and Δ11-comprehension rule. In Andrea Cantini, Ettore Casari, and Pierluigi Minari, editors, Logic and Foundation of Mathematics, pages 107--130. Kluwer, 1999. [ bib ] |
| [OW02] | Geoffrey E. Ostrin and Stanley S. Wainer. Proof theoretic complexity. In Helmut Schwichtenberg and Ralf Steinbrüggen, editors, Proof and System Reliability, volume 62 of NATO Science Series, pages 369--398. Springer, 2002. [ bib | .pdf ] |
| [OW05] | Geoffrey E. Ostrin and Stanley S. Wainer. Elementary arithmetic. Annals of Pure and Applied Logic, 133(1--3):275--292, 2005. [ bib | .pdf ] |
| [Pro99] | Dieter Probst. Dependent choice in explicit mathematics. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1999. [ bib | .pdf ] |
| [Pro05a] | Dieter Probst. On the relationship between fixed points and iteration in admissible set theory without foundation. Archive for Mathematical Logic, 44(5):561--580, 2005. [ bib | .pdf ] |
| [Pro05b] | Dieter Probst. Pseudo-Hierarchies in Admissible Set Theory without Foundation and Explicit Mathematics. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2005. [ bib | .pdf ] |
| [Pro06] | Dieter Probst. The proof-theoretic analysis of transfinitely iterated quasi least fixed points. The Journal of Symbolic Logic, 71(3):721--746, 2006. [ bib | .pdf ] |
| [Pro11] | Dieter Probst. The provably terminating operations of the subsystem PETJ of explicit mathematics. Annals of Pure and Applied Logic, 162(11):934--947, 2011. [ bib | DOI | .pdf ] |
| [Pro17] | Dieter Probst. A modular ordinal analysis of metapredicative subsystems of second order arithmetic. Habilitationsschrift, Universität Bern, Institut für Informatik und angewandte Mathematik, 2017. [ bib | .pdf ] |
| [PS01] | Dieter Probst and Thomas Studer. How to normalize the Jay. Theoretical Computer Science, 254(1--2):677--681, 2001. [ bib | .pdf ] |
| [PS11] | Dieter Probst and Thomas Strahm. Admissible closures of polynomial time computable arithmetic. Archive for Mathematical Logic, 50(5-6):643--660, 2011. [ bib | .pdf ] |
| [PS16] | Dieter Probst and Peter Schuster, editors. Concepts of Proof in Mathematics, Philosophy, and Computer Science, volume 6 of Ontos Mathematical Logic. Walter De Gruyter Incorporated, 2016. [ bib ] |
| [Pul10] | Cornelia Pulver. Self-Referentiality in Contraction-free Fragments of Modal Logic S4. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2010. [ bib | .pdf ] |
| [Ran15] | Florian Ranzi. From a Flexible Type System to Metapredicative Wellordering Proofs. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2015. [ bib | .pdf ] |
| [RS02] | Christian Rüede and Thomas Strahm. Intuitionistic fixed point theories for strictly positive operators. Mathematical Logic Quarterly, 48(2):195--202, 2002. [ bib | .pdf ] |
| [RS14] | Florian Ranzi and Thomas Strahm. A note on the theory SID<ω of stratified induction. Mathematical Logic Quarterly, 60(6):487--497, 2014. [ bib | DOI | .pdf ] |
| [Rüe00] | Christian Rüede. Metapredicative Subsystems of Analysis. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2000. [ bib | .pdf ] |
| [Rüe02] | Christian Rüede. Transfinite dependent choice and ω-model reflection. The Journal of Symbolic Logic, 67(3):1153--1168, 2002. [ bib | .pdf ] |
| [Rüe03a] | Christian Rüede. The proof-theoretic analysis of Σ11 transfinite dependent choice. Annals of Pure and Applied Logic, 122(1--3):195--234, 2003. [ bib | .pdf ] |
| [Rüe03b] | Christian Rüede. Universes in metapredicative analysis. Archive for Mathematical Logic, 42(2):129--151, 2003. [ bib | .pdf ] |
| [Sal05] | Vincenzo Salipante. On the Consistency Strength of the Strict Π11 Reflection Principle. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2005. [ bib | .pdf ] |
| [Sat14a] | Kentaro Sato. Forcing for Hat Inductive Definitions in Arithmetic -- One of the Simplest Applications of Forcing --. Mathematical Logic Quarterly, 60(4-5):314--318, 2014. [ bib | DOI | .pdf ] |
| [Sat14b] | Kentaro Sato. Relative predicativity and dependent recursion in second-order set theory and higher-order theories. The Journal of Symbolic Logic, 79:712--732, September 2014. [ bib | DOI | .pdf ] |
| [Sat15a] | Kentaro Sato. Full and hat inductive definitions are equivalent in nbg. Archive for Mathematical Logic, 54(1-2):75--112, 2015. [ bib | .pdf ] |
| [Sat15b] | Kentaro Sato. A new model construction by making a detour via intuitionistic theories ii: Interpretability lower bound of feferman's explicit mathematics t0. Annals of pure and applied logic, 166(7-8):800--835, 2015. [ bib | .pdf ] |
| [Sav12] | Yury Savateev. Product-free Lambek calculus is NP-complete. Annals of Pure and Applied Logic, 163(7):775--788, 2012. The Symposium on Logical Foundations of Computer Science 2009. [ bib | DOI | .pdf ] |
| [Sav14] | Yury Savateev. Proof Internalization for Generalized Frege Systems for Classical Logic. Annals of Pure and Applied Logic, 165(1):340--356, 2014. [ bib | DOI | .pdf ] |
| [Sch98a] | Stefan Schwendimann. Aspects of Computational Logic. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1998. [ bib | .ps ] |
| [Sch98b] | Stefan Schwendimann. A new one-pass tableau calculus for PLTL. In Harrie C. M. de Swart, editor, Proceedings of Tableaux '98, volume 1397 of Lecture Notes in Computer Science, pages 277--292. Springer, 1998. [ bib | .ps ] |
| [Sch03] | Thomas Schweizer. Two interpretations of WKL0 in subsystems of PA. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2003. [ bib | .pdf ] |
| [SDO17a] | Nenad Savić, Dragan Doder, and Zoran Ognjanović. A First-Order Logic for Reasoning About Higher-Order Upper and Lower Probabilities, page 491500. Springer International Publishing, Cham, 2017. [ bib | .pdf ] |
| [SDO17b] | Nenad Savić, Dragan Doder, and Zoran Ognjanović. Logics with lower and upper probability operators. International Journal of Approximate Reasoning, 88:148 -- 168, 2017. [ bib | .pdf ] |
| [SH98] | Holger Schlingloff and Wolfgang Heinle. Relation algebra and modal logics. In Chris Brink, Wolfram Kahl, and Gunther Schmidt, editors, Relational Methods in Computer Science, Advances in Computer Science, pages 20--89. Springer, 1998. [ bib ] |
| [Son05] | Daniel Sonderegger. PLTL -- Vollständigkeit und Modell-Konstruktion. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2005. [ bib | .pdf ] |
| [Spe05] | Daria Spescha. ALOE -- a graphical editor for OWL ontologies. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2005. [ bib | .pdf ] |
| [Spe09] | Daria Spescha. Weak Systems of Explicit Mathematics. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2009. [ bib | .pdf ] |
| [SS05] | Kilian Stoffel and Thomas Studer. Provable data privacy. In Kim Viborg Andersen, John K. Debenham, and Roland Wagner, editors, Proceedings of 16th International Conference on Database and Expert Systems Applications, volume 3588 of Lecture Notes in Computer Science, pages 324--332. Springer, 2005. [ bib | .pdf ] |
| [SS06] | David Steiner and Thomas Strahm. On the proof theory of type two functionals based on primitive recursive operations. Mathematical Logic Quarterly, 52(3):237--252, 2006. [ bib | .pdf ] |
| [SS07a] | David Steiner and Thomas Studer. Total public announcements. In Sergei Artemov and Anil Nerode, editors, Proceedings of Logical Foundations of Computer Science, volume 4514 of Lecture Notes in Computer Science, pages 498--511. Springer, 2007. [ bib | DOI | .pdf ] |
| [SS07b] | Phiniki Stouppa and Thomas Studer. A formal model of data privacy. In Irina Virbitskaite and Andrei Voronkov, editors, Proceedings of Perspectives of System Informatics, volume 4378 of Lecture Notes in Computer Science, pages 401--411. Springer, 2007. [ bib | .pdf ] |
| [SS09a] | Daria Spescha and Thomas Strahm. Elementary explicit types and polynomial time operations. Mathematical Logic Quarterly, 55(3):245 --258, 2009. [ bib | .pdf ] |
| [SS09b] | Phiniki Stouppa and Thomas Studer. Data Privacy for ALC Knowledge Bases. In S. Artemov and A. Nerode, editors, Proceedings of Logical Foundations of Computer Science LFCS'09, volume 5407 of LNCS, pages 409--421. Springer, 2009. [ bib | .pdf ] |
| [SS11] | Daria Spescha and Thomas Strahm. Realizability in weak systems of explicit mathematics. Mathematical Logic Quarterly, 57(6):551--565, 2011. [ bib | .pdf ] |
| [SS15] | Giovanni Sommaruga and Thomas Strahm, editors. Turings Revolution: The Impact of His Ideas about Computability. Birkhäuser, 2015. [ bib | http ] |
| [Ste01] | David Steiner. Proof-theoretic strength of PRON with various extensions. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2001. [ bib | .pdf ] |
| [Ste06] | David Steiner. A system for consistency preserving belief change. In Sergei Artemov and Rohit Parikh, editors, Proceedings of Rationality and Knowledge, 18th European Summer School of Logic, Language and Information, pages 133--144. Association for Logic, Language and Information, 2006. [ bib | .pdf ] |
| [Ste09] | David Steiner. Belief Change Functions for Multi-Agent Systems. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2009. [ bib | .pdf ] |
| [Sto07] | Phiniki Stouppa. A deep inference system for the modal logic S5. Studia Logica, 85(2):199--214, 2007. [ bib | DOI | .pdf ] |
| [Sto09] | Phiniki Stouppa. Deciding Data Privacy for ALC Knowledge Bases. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2009. [ bib | .pdf ] |
| [Sto10] | Manuela Claudia Stolz. Verification of Workflow Control-Flow Patterns with the SPIN Model Checker. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2010. [ bib ] |
| [Str94] | Tyko Strassen. The Basic Logic of Proofs. PhD thesis, University of Bern, April 1994. [ bib | .pdf ] |
| [Str96a] | Thomas Strahm. On the Proof Theory of Applicative Theories. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1996. [ bib | .ps ] |
| [Str96b] | Thomas Strahm. Partial applicative theories and explicit substitutions. Journal of Logic and Computation, 6(1):55--77, 1996. [ bib | .ps ] |
| [Str97] | Thomas Strahm. Polynomial time operations in explicit mathematics. The Journal of Symbolic Logic, 62(2):575--594, 1997. [ bib | .ps ] |
| [Str99] | Thomas Strahm. First steps into metapredicativity in explicit mathematics. In S. Barry Cooper and John K. Truss, editors, Sets and Proofs, volume 258 of London Mathematical Society Lecture Notes, pages 383--402. Cambridge University Press, 1999. [ bib | .pdf ] |
| [Str00a] | Thomas Strahm. Autonomous fixed point progressions and fixed point transfinite recursion. In Samuel S. Buss, Petr Hajek, and Pavel Pudlak, editors, Proceedings of Logic Colloquium '98, volume 13 of Association of Symbolic Logic Lecture Notes in Logic, pages 449--464. AK Peters, 2000. [ bib | .pdf ] |
| [Str00b] | Thomas Strahm. The non-constructive μ-operator, fixed point theories with ordinals, and the bar rule. Annals of Pure and Applied Logic, 104(1--3):305--324, 2000. [ bib | .ps ] |
| [Str01] | Thomas Strahm. Proof-theoretic contributions to explicit mathematics. Habilitationsschrift, Universität Bern, Institut für Informatik und angewandte Mathematik, 2001. [ bib | .pdf ] |
| [Str02] | Thomas Strahm. Wellordering proofs for metapredicative Mahlo. The Journal of Symbolic Logic, 67(1):260--278, 2002. [ bib | .pdf ] |
| [Str03] | Thomas Strahm. Theories with self-application and computational complexity. Information and Computation, 185(2):263--297, 2003. [ bib | .pdf ] |
| [Str04] | Thomas Strahm. A proof-theoretic characterization of the basic feasible functionals. Theoretical Computer Science, 329(1--3):159--176, 2004. [ bib | .pdf ] |
| [Str08a] | Thomas Strahm, editor. Gödel's Dialectica Interpretation. Number 62(2) in Dialectica. Wiley, special edition, 2008. [ bib | http ] |
| [Str08b] | Thomas Strahm. Introduction. Dialectica, 62(2):145--147, 2008. [ bib | DOI | .pdf ] |
| [Str10] | Thomas Strahm. Weak theories of operations and types. In Ralf Schindler, editor, Ways of Proof Theory, pages 441--468. Ontos Verlag, 2010. [ bib | .pdf ] |
| [Stu97] | Thomas Studer. Explicit mathematics: W-type, models. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1997. [ bib | .ps ] |
| [Stu99] | Thomas Studer. A semantics for λ{ }str: a calculus with overloading and late-binding. Technical Report IAM--99--004, Universität Bern, Institut für Informatik und angewandte Mathematik, 1999. [ bib | .ps ] |
| [Stu01a] | Thomas Studer. Constructive foundations for Featherweight Java. In Reinhard Kahle, Peter Schroeder-Heister, and Robert F. Stärk, editors, Proceedings of the International Seminar on Proof Theory in Computer Science, volume 2183 of Lecture Notes in Computer Science, pages 202--238. Springer, 2001. [ bib | .pdf ] |
| [Stu01b] | Thomas Studer. Object-Oriented Programming in Explicit Mathematics: Towards the Mathematics of Objects. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2001. [ bib | .pdf ] |
| [Stu01c] | Thomas Studer. A semantics for λ{ }str: a calculus with overloading and late-binding. Journal of Logic and Computation, 11(4):527--544, 2001. [ bib | .pdf ] |
| [Stu05a] | Thomas Studer. Explicit mathematics: power types and overloading. Annals of Pure and Applied Logic, 134(2--3):284--302, 2005. [ bib | .pdf ] |
| [Stu05b] | Thomas Studer. Papers in explicit mathematics. Technical report, Universität Bern, 2005. [ bib ] |
| [Stu05c] | Thomas Studer. Relational representation of ALN knowledge bases. In Pedro Isaías, Miguel B. Nunes, and Antonio Palma dos Reis, editors, Proceedings of Multi '05, pages 271--278. International Association for Development of the Information Society, 2005. [ bib | .pdf ] |
| [Stu08] | Thomas Studer. On the proof theory of the modal mu-calculus. Studia Logica, 89(3):343--363, 2008. [ bib | DOI | .pdf ] |
| [Stu09] | Thomas Studer. Common knowledge does not have the Beth property. Information Processing Letters, 109:611--614, 2009. [ bib | .pdf ] |
| [Stu10a] | Thomas Studer. Privacy Preserving Modules for Ontologies. In A. Pnueli, I. Virbitskaite, and A. Voronkov, editors, Proceedings of Perspectives of System Informatics PSI'09, volume 5947 of Lecture Notes in Computer Science, pages 380--387, 2010. [ bib | .pdf ] |
| [Stu10b] | Thomas Studer. Proof-Theoretic Contributions to Modal Fixed Point Logics. Habilitationsschrift, Universität Bern, Institut für Informatik und angewandte Mathematik, 2010. [ bib | .pdf ] |
| [Stu11a] | Thomas Studer. An application of justification logic to protocol verification. In Proceedings of Computational Intelligence and Security CIS 2011, pages 779--783. IEEE, 2011. [ bib | .pdf ] |
| [Stu11b] | Thomas Studer. Justification Logic, Inference Tracking, and Data Privacy. Logic and Logical Philosophy, 20(4):297--306, 2011. [ bib | .pdf ] |
| [Stu12] | Thomas Studer. Justified terminological reasoning. In E. Clarke, I. Virbitskaite, and A. Voronkov, editors, Proceedings of Perspectives of System Informatics PSI'11, volume 7162 of Lecture Notes in Computer Science, pages 349--361. Springer, 2012. [ bib | .pdf ] |
| [Stu13a] | Thomas Studer. A Universal Approach to Guarantee Data Privacy. Logica Universalis, 7(2):195--209, 2013. [ bib | .pdf ] |
| [Stu13b] | Thomas Studer. Decidability for some justification logics with negative introspection. The Journal of Symbolic Logic, 78(2):388--402, 2013. [ bib | .pdf ] |
| [SW14] | Thomas Studer and Johannes Werner. Censors for Boolean Description Logic. Transactions on Data Privacy, 7:223--252, 2014. [ bib | .pdf ] |
| [SY16] | Silvia Steila and Keita Yokoyama. Reverse mathematical bounds for the termination theorem. Annals of Pure and Applied Logic, 167(12):1213 -- 1241, 2016. [ bib | DOI | www: ] |
| [SZ08] | Thomas Strahm and Jeffery I Zucker. Primitive recursive selection functions for existential assertions over abstract algebras. Journal of Logic and Algebraic Programming, 76(2):175--197, 2008. [ bib | .pdf ] |
| [SZ15] | Kentaro Sato and Rico Zumbrunnen. A new model construction by making a detour via intuitionistic theories i: Operational set theory without choice is Π1-equivalent to kp. Annals of pure and applied logic, 166(2):121--186, 2015. [ bib | .pdf ] |
| [Tra09] | Roger Traber. Proof-Systems for PLTL: Cycling Sequents and their Use in a Finitization for PLTL. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2009. [ bib | .pdf ] |
| [Tup00] | Sergei Tupailo. Finitary reductions for local predicativity, I: recursively regular ordinals. In Samuel S. Buss, Petr Hajek, and Pavel Pudlak, editors, Proceedings of Logic Colloquium '98, volume 13 of Association of Symbolic Logic Lecture Notes in Logic, pages 465--499. AK Peters, 2000. [ bib ] |
| [Tup01] | Sergei Tupailo. Realization of analysis into explicit mathematics. The Journal of Symbolic Logic, 66(4):1848--1864, 2001. [ bib | .pdf ] |
| [Tup03] | Sergei Tupailo. Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe. Annals of Pure and Applied Logic, 120:165--196, 2003. [ bib | .ps ] |
| [Weh06a] | Ricardo Wehbe. A hybrid representation of knowledge and belief. In Proceedings of Formal Approaches to Multi-Agent Systems, 17th biennial European Conference on Artificial Intelligence, 2006. [ bib | .pdf ] |
| [Weh06b] | Ricardo Wehbe. Revising non-monotonic rule-based belief databases. In Proceedings of Belief Revision, Belief Merging and Social Choice, 8th Augustus De Morgan Workshop, 2006. [ bib | .pdf ] |
| [Weh07a] | Ricardo Wehbe. Computing with common knowledge. In Angel P. del Pobil, editor, Proceedings of Artificial Intelligence and Soft Computing, pages 45--50. ACTA Press, 2007. [ bib | .pdf ] |
| [Weh07b] | Ricardo Wehbe. Merging rule-based belief databases. In Vladan Devedžić, editor, Proceedings of Artificial Intelligence and Applications, pages 585--589. ACTA Press, 2007. [ bib | .pdf ] |
| [Weh10] | Ricardo Wehbe. Annotated Systems for Common Knowledge. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2010. [ bib | .pdf ] |
| [Wir99a] | Marc Wirz. Characterizing the Grzegorczyk hierarchy by safe recursion. Technical Report IAM--99--005, Universität Bern, Institut für Informatik und angewandte Mathematik, 1999. [ bib | .pdf ] |
| [Wir99b] | Marc Wirz. Charakterisierungen kleiner Komplexitätsklassen mittels geschichteter N-Prädikate. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 1999. [ bib | .pdf ] |
| [Wir05] | Marc Wirz. Wellordering Two Sorts: A Slow-Growing Proof Theory for Variable Separation. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2005. [ bib | .pdf ] |
| [WS15] | Johannes Martin Werner and T. Studer. Controlled Query Evaluation in General Semantics with Incomplete Information. PhD thesis, Institut für Informatik und angewandte Mathematik, March 2015. ISBN 978-1-326-21681-8. [ bib | .pdf ] |
| [Zum09] | Rico Zumbrunnen. Ontological Questions about Operational Set Theory. Master's thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2009. [ bib | .pdf ] |
| [Zum13] | Rico Zumbrunnen. Contributions to Operational Set Theory. PhD thesis, Universität Bern, Institut für Informatik und angewandte Mathematik, 2013. [ bib | .pdf ] |
This file was generated by bibtex2html 1.99.