-
550From Display to Labelled Proofs for Tense LogicsIn 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.
-
488The Basics of Display CalculiKriterion - 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.
-
439Cut-free Calculi and Relational Semantics for Temporal STIT LogicsIn 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
-
421The Varieties of Ought-implies-Can and Deontic STIT LogicIn Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science (Lecture Notes in Computer Science 7734), Springer. 2013.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
-
416A Decidable Multi-agent Logic for Reasoning About Actions, Instruments, and NormsIn 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
-
401Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT LogicsIn 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
-
386A Neutral Temporal Deontic STIT LogicIn 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
-
342Refining Labelled Systems for Modal and Constructive Logics with ApplicationsDissertation, 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
-
339On Deriving Nested Calculi for Intuitionistic Logics from Semantic SystemsIn Sergei Artemov & Anil Nerode (eds.), Logical Foundations of Computer Science (Lecture Notes in Computer Science 7734), Springer. pp. 177-194. 2013.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
-
333Nested Sequents for Intuitionistic Modal Logics via Structural RefinementIn Anupam Das & Sara Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods: TABLEAUX 2021. pp. 409-427. 2021.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
-
305Automating Reasoning with Standpoint Logic via Nested SequentsIn Michael Thielscher, Francesca Toni & Frank Wolter (eds.), Proceedings of the Sixteenth International Conference on Principles of Knowledge Representation and Reasoning (KR2018). pp. 257-266. 2018.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
-
302Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested SequentsIn 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
-
295Display to Labeled Proofs and Back Again for Tense LogicsACM 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
-
282On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic LogicsJournal 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
-
282A Framework for Intuitionistic Grammar LogicsIn 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.
-
205Uniform and Modular Sequent Systems for Description LogicsIn 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
-
30A logical analysis of instrumentality judgments: means-end relations in the context of experience and expectationsJournal of Philosophical Logic 52 (5). 2023.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
-
21Nested sequents for intermediate logics: the case of Gödel-Dummett logicsJournal 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
Technische Universität Wien
Alumnus, 2021
Dresden, SN, Germany
Areas of Specialization
Science, Logic, and Mathematics |
Areas of Interest
Science, Logic, and Mathematics |