The Experts below are selected from a list of 249 Experts worldwide ranked by ideXlab platform

Eric Pacuit - One of the best experts on this subject based on the ideXlab platform.

  • Neighbourhood structures : bisimilarity and basic model theory
    Logical Methods in Computer Science, 2009
    Co-Authors: Helle Hvid Hansen, Clemens Kupke, Eric Pacuit
    Abstract:

    Neighbourhood structures are the standard semantic tool used to reason about non-normal Modal Logics. The Logic of all neighbourhood models is called Classical Modal Logic. In coalgebraic terms, a neighbourhood frame is a coalgebra for the contravariant powerset functor composed with itself, denoted by 2 2 . We use this coalgebraic modelling to derive notions of equivalence between neighbourhood structures. 2 2 -bisimilarity and behavioural equivalence are well known coalgebraic concepts, and they are distinct, since 2 2 does not preserve weak pullbacks. We introduce a third, intermediate notion whose wit- nessing relations we call precocongruences (based on pushouts). We give back-and-forth style characterisations for 2 2 -bisimulations and precocongruences, we show that on a single coalgebra, precocongruences capture behavioural equivalence, and that between neighbour- hood structures, precocongruences are a better approximation of behavioural equivalence than 2 2 -bisimulations. We also introduce a notion of Modal saturation for neighbourhood models, and investigate its relationship with denability and image-niteness. We prove a Hennessy-Milner theorem for Modally saturated and for image-nite neighbourhood mod- els. Our main results are an analogue of Van Benthem's characterisation theorem and a model-theoretic proof of Craig interpolation for Classical Modal Logic.

  • First-Order Classical Modal Logic
    Studia Logica, 2006
    Co-Authors: Horacio Arló-costa, Eric Pacuit
    Abstract:

    The paper focuses on extending to the first order case the semantical program for Modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer in the first part of the paper a series of new completeness results for salient Classical systems of first order Modal Logic. Among other results we show that it is possible to prove strong completeness results for normal systems without the Barcan Formula (like FOL + K )in terms of neighborhood frames with constant domains. The first order models we present permit the study of many epistemic Modalities recently proposed in computer science as well as the development of adequate models for monadic operators of high probability. Models of this type are either difficult of impossible to build in terms of relational Kripkean semantics [40]. We conclude by introducing general first order neighborhood frames with constant domains and we offer a general completeness result for the entire family of Classical first order Modal systems in terms of them, circumventing some well-known problems of propositional and first order neighborhood semantics (mainly the fact that many Classical Modal Logics are incomplete with respect to an unmodified version of either neighborhood or relational frames). We argue that the semantical program that thus arises offers the first complete semantic unification of the family of Classical first order Modal Logics.

  • first order Classical Modal Logic applications in Logics of knowledge and probability
    Theoretical Aspects of Rationality and Knowledge, 2005
    Co-Authors: Horacio Arlocosta, Eric Pacuit
    Abstract:

    The paper focuses on extending to the first order case the semantical program for Modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer a series of new completeness results for salient Classical systems of first order Modal Logic. Among other results we show that it is possible to prove strong completeness results for normal systems without the Barcan Formula (like FOL + K) in terms of neighborhood frames with constant domains. The first order models we present permit the study of many epistemic Modalities recently proposed in computer science as well as the development of adequate models for monadic operators of high probability. We conclude by offering a general completeness result for the entire family of first order Classical Modal Logics (encompassing both normal and non-normal systems).

  • TARK - First-order Classical Modal Logic: applications in Logics of knowledge and probability
    2005
    Co-Authors: Horacio Arló-costa, Eric Pacuit
    Abstract:

    The paper focuses on extending to the first order case the semantical program for Modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer a series of new completeness results for salient Classical systems of first order Modal Logic. Among other results we show that it is possible to prove strong completeness results for normal systems without the Barcan Formula (like FOL + K) in terms of neighborhood frames with constant domains. The first order models we present permit the study of many epistemic Modalities recently proposed in computer science as well as the development of adequate models for monadic operators of high probability. We conclude by offering a general completeness result for the entire family of first order Classical Modal Logics (encompassing both normal and non-normal systems).

Sumit Sourabh - One of the best experts on this subject based on the ideXlab platform.

  • Order theoretic Correspondence for Intuitionistic mu-calculus
    2020
    Co-Authors: Sumit Sourabh
    Abstract:

    Sahlqvist correspondence theory [3], [4] is one of the most important and useful results of Classical Modal Logic. It gives a syntactic identication of a class of Modal formulas whose associated normal Modal Logics are strongly complete with respect to elementary (i.e. rst-order denable)

  • Correspondence and canonicity in non-Classical Logic
    2020
    Co-Authors: Sumit Sourabh
    Abstract:

    In this thesis we study correspondence and canonicity for non-Classical Logic using algebraic and order-topoLogical methods. Correspondence theory is aimed at answering the question of how precisely Modal, first-order, second-order languages interact and overlap in their shared semantic environment. The line of research in correspondence theory which concerns the present thesis is Sahlqvist correspondence theory --- which was originally developed for Classical Modal Logic, and provides a systematic translation between Classical Modal Logic and first-order Logic. Canonicity is closely related to correspondence, and ensures that Logics axiomatized by these formulas are complete with respect to relational semantics. Thus, correspondence and canonicity together establish that Sahlqvist Logics are semantically complete with respect to first-order definable classes of relational structures. The first part of the thesis focuses on algebraic methods. In chapter 3, we prove the Classical Sahlqvist correspondence theorem for basic Modal Logic in the algebraic setting of complex algebras of frames. We extend the algorithm ALBA to regular Modal Logic (Modal Logic with non-normal Modalities) and intuitionistic Modal mu-calculus in Chapters 4 and 5, respectively. In Chapter 6, we develop ALBA for distributive lattice expansions, using which we prove relativised canonicity for the meta-inductive inequalities. The second part of the thesis focuses on order-topoLogical methods. In Chapter 7, we prove a Modal-like duality for de Vries algebras. In Chapter 8, we prove a Sahlqvist correspondence and canonicity theorem for topoLogical fixed-point Logic on compact Hausdorff spaces.

  • Algebraic Modal correspondence: Sahlqvist and beyond
    The Journal of Logic and Algebraic Programming, 2017
    Co-Authors: Willem Conradie, Alessandra Palmigiano, Sumit Sourabh
    Abstract:

    The present paper proposes a new introductory treatment of the very well known Sahlqvist correspondence theory for Classical Modal Logic. The first motivation for the present treatment is a consideration regarding exposition: Classical Sahlqvist correspondence is presented in a uniform and modular way, and, unlike the existing textbook accounts, extends itself to a class of formulas laying outside the Sahlqvist class proper. The second motivation is methodoLogical: the present treatment aims at highlighting the algebraic and order-theoretic nature of the correspondence mechanism. The exposition remains elementary and does not presuppose any previous knowledge or familiarity with the algebraic approach to Logic. However, it provides the underlying motivation and basic intuitions for the recent developments in the Sahlqvist theory of nonClassical Logics, which compose the so-called unified correspondence theory.

  • Algebraic Modal correspondence: Sahlqvist and beyond
    arXiv: Logic, 2016
    Co-Authors: Willem Conradie, Alessandra Palmigiano, Sumit Sourabh
    Abstract:

    The present paper proposes a new introductory treatment of the very well known Sahlqvist correspondence theory for Classical Modal Logic. The first motivation for the present treatment is {\em pedagogical}: Classical Sahlqvist correspondence is presented in a uniform and modular way, and, unlike the existing textbook accounts, extends itself to a class of formulas laying outside the Sahlqvist class proper. The second motivation is {\em methodoLogical}: the present treatment aims at highlighting the {\em algebraic} and {\em order-theoretic} nature of the correspondence mechanism. The exposition remains elementary and does not presuppose any previous knowledge or familiarity with the algebraic approach to Logic. However, it provides the underlying motivation and basic intuitions for the recent developments in the Sahlqvist theory of nonClassical Logics, which compose the so-called unified correspondence theory.

  • Canonicity and Relativized Canonicity via Pseudo-Correspondence: an Application of ALBA.
    arXiv: Logic in Computer Science, 2015
    Co-Authors: Willem Conradie, Sumit Sourabh, Alessandra Palmigiano, Zhiguang Zhao
    Abstract:

    We generalize Venema's result on the canonicity of the additivity of positive terms, from Classical Modal Logic to a vast class of Logics the algebraic semantics of which is given by varieties of normal distributive lattice expansions (normal DLEs), aka `distributive lattices with operators'. We provide two contrasting proofs for this result: the first is along the lines of Venema's pseudo-correspondence argument but using the insights and tools of unified correspondence theory, and in particular the algorithm ALBA; the second closer to the style of Jonsson. Using insights gleaned from the second proof, we define a suitable enhancement of the algorithm ALBA, which we use prove the canonicity of certain syntactically defined classes of DLE-inequalities (called the meta-inductive inequalities), relative to the structures in which the formulas asserting the additivity of some given terms are valid.

Horacio Arlocosta - One of the best experts on this subject based on the ideXlab platform.

  • first order Classical Modal Logic applications in Logics of knowledge and probability
    Theoretical Aspects of Rationality and Knowledge, 2005
    Co-Authors: Horacio Arlocosta, Eric Pacuit
    Abstract:

    The paper focuses on extending to the first order case the semantical program for Modalities first introduced by Dana Scott and Richard Montague. We focus on the study of neighborhood frames with constant domains and we offer a series of new completeness results for salient Classical systems of first order Modal Logic. Among other results we show that it is possible to prove strong completeness results for normal systems without the Barcan Formula (like FOL + K) in terms of neighborhood frames with constant domains. The first order models we present permit the study of many epistemic Modalities recently proposed in computer science as well as the development of adequate models for monadic operators of high probability. We conclude by offering a general completeness result for the entire family of first order Classical Modal Logics (encompassing both normal and non-normal systems).

Giovanna D'agostino - One of the best experts on this subject based on the ideXlab platform.

  • Uniform interpolation for propositional and Modal team Logics
    Journal of Logic and Computation, 2019
    Co-Authors: Giovanna D'agostino
    Abstract:

    Abstract In this paper we consider Modal team Logic, a generalization of Classical Modal Logic in which it is possible to describe dependence phenomena between data. We prove that most known fragments of full Modal team Logic allow the elimination of the so called ‘existential bisimulation quantifiers’, where the existence of a certain set is required only modulo bisimulation (i.e. not in the model itself but possibly in a bisimilar model). As a consequence, we prove that these fragments enjoy the uniform interpolation property.

  • Uniform Interpolation for Propositional and Modal Team Logics.
    arXiv: Logic in Computer Science, 2018
    Co-Authors: Giovanna D'agostino
    Abstract:

    In this paper we consider Modal Team Logic, a generalization of Classical Modal Logic in which it is possible to describe dependence phenomena between data. We prove that most known fragment of Full Modal Team Logic allow the elimination of the so called "existential bisimulation quantifiers", where the existence of a certain set is made modulo bisimulation. As a consequence, we prove that these fragments enjoy the Uniform Interpolation Property.

Armando Tacchella - One of the best experts on this subject based on the ideXlab platform.

  • System description : *SAT a platform for the development of Modal decision procedures
    Lecture Notes in Computer Science, 2020
    Co-Authors: Enrico Giunchiglia, Armando Tacchella
    Abstract:

    * SAT is a platform for the development of Modal decision procedures. Currently, * SAT features decision procedures for the normal Modal Logic K(m) and for the Classical Modal Logic E(m). * SAT embodies a state of the art SAT solver, and includes techniques for optimizing automated deduction in Modal and temporal Logics. Owing to its modular design and to the extensive reuse of software components, * SAT provides an open, easy to maintain, yet efficient implementation framework.

  • CADE - System Description: *SAT: A Platform for the Development of Modal Decision Procedures
    Automated Deduction - CADE-17, 2000
    Co-Authors: Enrico Giunchiglia, Armando Tacchella
    Abstract:

    *sat is a platform for the development of Modal decision procedures. Currently, *sat features decision procedures for the normal Modal Logic K(m) and for the Classical Modal Logic E(m). *sat embodies a state of the art sat solver, and includes techniques for optimizing automated deduction in Modal and temporal Logics. Owing to its modular design and to the extensive reuse of software components, *sat provides an open, easy to maintain, yet efficient implementation framework.