Technische Universität Wien
Alumnus, 2021
Dresden, SN, Germany
Areas of Specialization
Science, Logic, and Mathematics
  •  550
    From Display to Labelled Proofs for Tense Logics
    with Agata Ciabattoni and Revantha Ramanayake
    In Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science (Lecture Notes in Computer Science 7734), Springer. 2013.
    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.
  •  488
    The Basics of Display Calculi
    with Christian Ittner, Timo Eckhardt, and Norbert Gratzl
    Kriterion - Journal of Philosophy 31 (2): 55-100. 2017.
    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.
  •  439
    Cut-free Calculi and Relational Semantics for Temporal STIT Logics
    with Kees van Berkel
    In Francesco Calimeri, Nicola Leone & Marco Manna (eds.), Logics in Artificial Intelligence, Springer. 2019.
    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 re…Read more
  •  421
    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 so…Read more
  •  416
    A Decidable Multi-agent Logic for Reasoning About Actions, Instruments, and Norms
    with Kees van Berkel and Francesco Olivieri
    In Johan van Benthem (ed.), Logic and argumentation, North-holland. 1996.
    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, …Read more
  •  401
    Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics
    with Kees van Berkel
    In M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems, Springer. pp. 202-218. 2019.
    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, resultin…Read more
  •  386
    A Neutral Temporal Deontic STIT Logic
    with Kees van Berkel
    In P. Blackburn, E. Lorini & M. Guo (eds.), Logic, Rationality, and Interaction, Springer. pp. 340-354. 2019.
    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 t…Read more
  •  342
    Refining Labelled Systems for Modal and Constructive Logics with Applications
    Dissertation, Technischen Universität Wien. 2021.
    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, l…Read more
  •  339
    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, sh…Read more
  •  333
    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 propa…Read more
  •  305
    Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics---proof systems that manipulate trees whose nodes are multisets of formulae---and show how to automate standpoint reasoning by means of non-deterministi…Read more
  •  302
    Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents
    with Alwen Tiu, Rajeev Gore, and Ranald Clouston
    In Maribel Fernandez & Anca Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). pp. 1-16. 2020.
    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 c…Read more
  •  295
    Display to Labeled Proofs and Back Again for Tense Logics
    with Agata Ciabattoni, Revantha Ramanayake, and Alwen Tiu
    ACM Transactions on Computational Logic 22 (3): 1-31. 2021.
    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 for…Read more
  •  282
    On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics
    Journal of Logic and Computation 31 (1): 213-265. 2021.
    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 …Read more
  •  282
    A Framework for Intuitionistic Grammar Logics
    In O. Stock & M. Schaerf (eds.), Lecture Notes In Computer Science, Springer Verlag. pp. 495-503. 2006.
    We generalize intuitionistic tense logics to the multi-modal case by placing grammar logics on an intuitionistic footing. We provide axiomatizations for a class of base intuitionistic grammar logics as well as provide axiomatizations for extensions with combinations of seriality axioms and what we call "intuitionistic path axioms". We show that each axiomatization is sound and complete with completeness being shown via a typical canonical model construction.
  •  205
    Uniform and Modular Sequent Systems for Description Logics
    with Jonas Karge
    In Ofer Arieli, Martin Homola, Jean Christoph Jung & Marie-Laure Mugnier (eds.), Proceedings of the 35th International Workshop on Description Logics (DL 2022). 2022.
    We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. Our framework not only covers a wide array of common description logics, but also allows for sequent systems to be obtained for extensions of description logics with special formulae that we call "role relational axioms." All sequent systems are sound, complete, and possess favorable properties such as height-preserving admissibility of common structural rules and height-…Read more
  •  30
    This article proposes the use of temporal logic for an analysis of instrumentality inspired by the work of G.H. von Wright. The first part of the article contains the philosophical foundations. We discuss von Wright’s general theory of agency and his account of instrumentality. Moreover, we propose several refinements to this framework via rigorous definitions of the core notions involved. In the second part, we develop a logical system called Temporal Logic of Action and Expectations (TLAE). Th…Read more
  •  21
    Nested sequents for intermediate logics: the case of Gödel-Dummett logics
    Journal of Applied Non-Classical Logics 33 (2): 121-164. 2023.
    We present nested sequent systems for propositional Gödel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these Gödel-Dummett logics, we introduce a new structural rule, called the linearity rule, which (bottom-up) operates by linearising branching structure in a given nested sequent. In addition, an interesting feature of our calculi is the inclusion of reachability rules, whic…Read more