
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): 55100. 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, firstorder, and modal display calculi are considered and their properties detailed.

439Cutfree Calculi and Relational Semantics for Temporal STIT LogicsIn Francesco Calimeri, Nicola Leone & Marco Manna (eds.), Logics in Artificial Intelligence, Springer. 2019.We present cutfree 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 cutadmissibility. 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 OughtimpliesCan 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 multiagent choicemaking. In the available deontic extensions of STIT, the principle of OughtimpliesCan (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 Multiagent Logic for Reasoning About Actions, Instruments, and NormsIn Johan van Benthem (ed.), Logic and argumentation, Northholland. 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 multiagent 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: ProofCalculi and Syntactic Decidability for STIT LogicsIn M. Baldoni, M. Dastani, B. Liao, Y. Sakurai & R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of MultiAgent Systems, Springer. pp. 202218. 2019.This work provides proofsearch algorithms and automated countermodel extraction for a class of STIT logics. With this, we answer an open problem concerning syntactic decision procedures and cutfree calculi for STIT logics. A new class of cutfree complete labelled sequent calculi G3LdmL^m_n, for multiagent STIT with at most nmany 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. 340354. 2019.In this work we answer a long standing request for temporal embeddings of deontic STIT logics by introducing the multiagent 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 prooftheoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cutfree calculi in possession of desirable prooftheoretic 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. 177194. 2013.This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and firstorder 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. 409427. 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. 257266. 2018.Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multiperspective 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 logicsproof systems that manipulate trees whose nodes are multisets of formulaeand show how to automate standpoint reasoning by means of nondeterministi…Read more

302Syntactic Interpolation for Tense Logics and BiIntuitionistic Logic via Nested SequentsIn Maribel Fernandez & Anca Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). pp. 116. 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 biintuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzenstyle sequent calculus, but have all been shown to have cutfree 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): 131. 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): 213265. 2021.This paper studies the relationship between labelled and nested calculi for propositional intuitionistic logic, firstorder intuitionistic logic with nonconstant domains and firstorder 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. 495503. 2006.We generalize intuitionistic tense logics to the multimodal 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 & MarieLaure 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 heightpreserving admissibility of common structural rules and height…Read more

30A logical analysis of instrumentality judgments: meansend 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ödelDummett logicsJournal of Applied NonClassical Logics 33 (2): 121164. 2023.We present nested sequent systems for propositional GödelDummett logic and its firstorder extensions with nonconstant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these GödelDummett logics, we introduce a new structural rule, called the linearity rule, which (bottomup) 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 