12 found
Sort by:
  1. Thomas Studer (2013). A Universal Approach to Guarantee Data Privacy. Logica Universalis 7 (2):195-209.
    The problem of data privacy is to verify that confidential information stored in an information system is not provided to unauthorized users and, therefore, personal and other sensitive data remain private. One way to guarantee this is to distort a knowledge base such that it does not reveal sensitive information. In the present paper we will give a universal definition of the problem of knowledge base distortion. It is universal in the sense that is independent of any particular knowledge representation (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  2. Thomas Studer (2013). Decidability for Some Justification Logics with Negative Introspection. Journal of Symbolic Logic 78 (2):388-402.
    Justification logics are modal logics that include justifications for the agent's knowledge. So far, there are no decidability results available for justification logics with negative introspection. In this paper, we develop a novel model construction for such logics and show that justification logics with negative introspection are decidable for finite constant specifications.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. Kai Brünnler & Thomas Studer (2012). Syntactic Cut-Elimination for a Fragment of the Modal Mu-Calculus. Annals of Pure and Applied Logic 163 (12):1838-1853.
    For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius [15] for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge [5] and by Hill and Poggiolesi for PDL[8], which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach can (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  4. Samuel Bucheli, Roman Kuznets & Thomas Studer (2011). Justifications for Common Knowledge. Journal of Applied Non-Classical Logics 21 (1):35-60.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  5. Gerhard Jäger & Thomas Studer (2011). A Buchholz Rule for Modal Fixed Point Logics. Logica Universalis 5 (1):1-19.
    Buchholz’s Ω μ+1-rules provide a major tool for the proof-theoretic analysis of arithmetical inductive definitions. The aim of this paper is to put this approach into the new context of modal fixed point logic. We introduce a deductive system based on an Ω-rule tailored for modal fixed point logic and develop the basic techniques for establishing soundness and completeness of the corresponding system. In the concluding section we prove a cut elimination and collapsing result similar to that of Buchholz (Iterated (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  6. Thomas Studer (2011). Justification Logic, Inference Tracking, and Data Privacy. Logic and Logical Philosophy 20 (4):297-306.
    Internalization is a key property of justification logics. It states that justification logics internalize their own notion of proof which is essential for the proof of the realization theorem. The aim of this note is to show how to make use of internalization to track where an agent’s knowledge comes from and how to apply this to the problem of data privacy.
    Direct download (12 more)  
     
    My bibliography  
     
    Export citation  
  7. Kai Brünnler & Thomas Studer (2009). Syntactic Cut-Elimination for Common Knowledge. Annals of Pure and Applied Logic 160 (1):82-95.
    We first look at an existing infinitary sequent system for common knowledge for which there is no known syntactic cut-elimination procedure and also no known non-trivial bound on the proof-depth. We then present another infinitary sequent system based on nested sequents that are essentially trees and with inference rules that apply deeply inside these trees. Thus we call this system “deep” while we call the former system “shallow”. In contrast to the shallow system, the deep system allows one to give (...)
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  8. Kai Brünnler, Dieter Probst & Thomas Studer (2008). On Contraction and the Modal Fragment. Mathematical Logic Quarterly 54 (4):345-349.
    We observe that removing contraction from a standard sequent calculus for first-order predicate logic preserves completeness for the modal fragment.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  9. Thomas Studer (2008). On the Proof Theory of the Modal Mu-Calculus. Studia Logica 89 (3):343 - 363.
    We study the proof-theoretic relationship between two deductive systems for the modal mu-calculus. First we recall an infinitary system which contains an omega rule allowing to derive the truth of a greatest fixed point from the truth of each of its (infinitely many) approximations. Then we recall a second infinitary calculus which is based on non-well-founded trees. In this system proofs are finitely branching but may contain infinite branches as long as some greatest fixed point is unfolded infinitely often along (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  10. Thomas Studer (2005). Explicit Mathematics: Power Types and Overloading. Annals of Pure and Applied Logic 134 (2-3):284-302.
    Systems of explicit mathematics provide an axiomatic framework for representing programs and proving properties of them. We introduce such a system with a new form of power types using a monotone power type generator. These power types allow us to model impredicative overloading. This is a very general form of type dependent computation which occurs in the study of object-oriented programming languages. We also present a set-theoretic interpretation for monotone power types. Thus establishing the consistency our system of explicit mathematics.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  11. Gerhard Jäger & Thomas Studer (2002). Extending the System of Explicit Mathematics: The Limit and Mahlo Axioms. Annals of Pure and Applied Logic 114 (1-3):79-101.
    In this paper we discuss extensions of Feferman's theory T 0 for explicit mathematics by the so-called limit and Mahlo axioms and present a novel approach to constructing natural recursion-theoretic models for systems of explicit mathematics which is based on nonmonotone inductive definitions.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  12. Gerhard Jäger, Reinhard Kahle & Thomas Studer (2001). Universes in Explicit Mathematics. Annals of Pure and Applied Logic 109 (3):141-162.
    This paper deals with universes in explicit mathematics. After introducing some basic definitions, the limit axiom and possible ordering principles for universes are discussed. Later, we turn to least universes, strictness and name induction. Special emphasis is put on theories for explicit mathematics with universes which are proof-theoretically equivalent to Feferman's.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation