Order:
See also
Tim Lyon
Technische Universität Dresden
  1.  20
    Display to Labeled Proofs and Back Again for Tense Logics.Agata Ciabattoni, Tim Lyon, Revantha Ramanayake & Alwen Tiu - 2021 - ACM Transactions on Computational Logic 22 (3):1-31.
    We introduce translations between display calculus proofs and labeled calculus proofs in the context of tense logics. First, we show that every derivation in the display calculus for the minimal tense logic Kt extended with general path axioms can be effectively transformed into a derivation in the corresponding labeled calculus. Concerning the converse translation, we show that for Kt extended with path axioms, every derivation in the corresponding labeled calculus can be put into a special form that is translatable to (...)
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  2.  33
    On the Correspondence Between Nested Calculi and Semantic Systems for Intuitionistic Logics.Tim Lyon - 2021 - Journal of Logic and Computation 31 (1):213-265.
    This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, first-order intuitionistic logic with non-constant domains and first-order intuitionistic logic with constant domains. It is shown that Fitting’s nested calculi naturally arise from their corresponding labelled calculi—for each of the aforementioned logics—via the elimination of structural rules in labelled derivations. The translational correspondence between the two types of systems is leveraged to show that the nested calculi inherit proof-theoretic properties from their associated labelled calculi, such as (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  3.  55
    Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic Via Nested Sequents.Tim Lyon, Alwen Tiu, Rajeev Gore & Ranald Clouston - 2020 - In Maribel Fernandez & Anca Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Dagstuhl, Germany: pp. 1-16.
    We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  4. From Display to Labelled Proofs for Tense Logics.Agata Ciabattoni, Tim Lyon & Revantha Ramanayake - 2018 - In Anil Nerode & Sergei Artemov (eds.), Logical Foundations of Computer Science. Springer International Publishing. pp. 120 - 139.
    We introduce an effective translation from proofs in the display calculus to proofs in the labelled calculus in the context of tense logics. We identify the labelled calculus proofs in the image of this translation as those built from labelled sequents whose underlying directed graph possesses certain properties. For the basic normal tense logic Kt, the image is shown to be the set of all proofs in the labelled calculus G3Kt.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  5.  75
    On Deriving Nested Calculi for Intuitionistic Logics From Semantic Systems.Tim Lyon - 2020 - In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science. Cham: pp. 177-194.
    This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and first-order intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable proof-theoretic properties from its associated (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  6. Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems. 93413 Cham, Germany: Springer. pp. 202-218.
    This work provides proof-search algorithms and automated counter-model extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cut-free calculi for STIT logics. A new class of cut-free complete labelled sequent calculi G3LdmL^m_n, for multi-agent STIT with at most n-many choices, is introduced. We refine the calculi G3LdmL^m_n through the use of propagation rules and demonstrate the admissibility of their structural rules, resulting in auxiliary calculi Ldm^m_nL. In the single-agent case, we (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  94
    A Neutral Temporal Deontic STIT Logic.Kees van Berkel & Tim Lyon - 2019 - In P. Blackburn, E. Lorini & M. Guo (eds.), Logic, Rationality, and Interaction. Berlin, Heidelberg: pp. 340-354.
    In this work we answer a long standing request for temporal embeddings of deontic STIT logics by introducing the multi-agent STIT logic TDS . The logic is based upon atemporal utilitarian STIT logic. Yet, the logic presented here will be neutral: instead of committing ourselves to utilitarian theories, we prove the logic TDS sound and complete with respect to relational frames not employing any utilitarian function. We demonstrate how these neutral frames can be transformed into utilitarian temporal frames, while preserving (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  8. Cut-Free Calculi and Relational Semantics for Temporal STIT Logics.Tim Lyon & Kees van Berkel - 2019 - In Francesco Calimeri, Nicola Leone & Marco Manna (eds.), Logics in Artificial Intelligence. Springer International Publishing. pp. 803 - 819.
    We present cut-free labelled sequent calculi for a central formalism in logics of agency: STIT logics with temporal operators. These include sequent systems for Ldm , Tstit and Xstit. All calculi presented possess essential structural properties such as contraction- and cut-admissibility. The labelled calculi G3Ldm and G3Tstit are shown sound and complete relative to irreflexive temporal frames. Additionally, we extend current results by showing that also Xstit can be characterized through relational frames, omitting the use of BT+AC frames.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  9.  17
    Nested Sequents for Intuitionistic Modal Logics Via Structural Refinement.Tim Lyon - 2021 - In Anupam Das & Sara Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021. 93413 Cham, Germany: pp. 409-427.
    We employ a recently developed methodology -- called "structural refinement" -- to extract nested sequent systems for a sizable class of intuitionistic modal logics from their respective labelled sequent systems. This method can be seen as a means by which labelled sequent systems can be transformed into nested sequent systems through the introduction of propagation rules and the elimination of structural rules, followed by a notational translation. The nested systems we obtain incorporate propagation rules that are parameterized with formal grammars, (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  10.  29
    Refining Labelled Systems for Modal and Constructive Logics with Applications.Tim Lyon - 2021 - Dissertation, Technischen Universität Wien
    This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates the (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  11.  89
    The Varieties of Ought-Implies-Can and Deontic STIT Logic.Kees van Berkel & Tim Lyon - 2021 - In Fenrong Liu, Alessandra Marra, Paul Portner & Frederik Van De Putte (eds.), Deontic Logic and Normative Systems: 15th International Conference.
    STIT logic is a prominent framework for the analysis of multi-agent choice-making. In the available deontic extensions of STIT, the principle of Ought-implies-Can (OiC) fulfills a central role. However, in the philosophical literature a variety of alternative OiC interpretations have been proposed and discussed. This paper provides a modular framework for deontic STIT that accounts for a multitude of OiC readings. In particular, we discuss, compare, and formalize ten such readings. We provide sound and complete sequent-style calculi for all of (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  12. The Basics of Display Calculi.Tim Lyon, Christian Ittner, Timo Eckhardt & Norbert Gratzl - 2017 - Kriterion - Journal of Philosophy 31 (2):55-100.
    The aim of this paper is to introduce and explain display calculi for a variety of logics. We provide a survey of key results concerning such calculi, though we focus mainly on the global cut elimination theorem. Propositional, first-order, and modal display calculi are considered and their properties detailed.
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  13. A Decidable Multi-Agent Logic for Reasoning About Actions, Instruments, and Norms.Kees van Berkel, Tim Lyon & Francesco Olivieri - 2020 - In Mehdi Dastani, Huimin Dong & Leon van der Torre (eds.), Logic and Argumentation. pp. 219 - 241.
    We formally introduce a novel, yet ubiquitous, category of norms: norms of instrumentality. Norms of this category describe which actions are obligatory, or prohibited, as instruments for certain purposes. We propose the Logic of Agency and Norms (LAN) that enables reasoning about actions, instrumentality, and normative principles in a multi-agent setting. Leveraging LAN , we formalize norms of instrumentality and compare them to two prevalent norm categories: norms to be and norms to do. Last, we pose principles relating the three (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark