-
12Hybrid Partial Type TheoryJournal of Symbolic Logic 1-43. forthcoming.In this article we define a logical system called Hybrid Partial Type Theory ( $\mathcal {HPTT}$ ). The system is obtained by combining William Farmer’s partial type theory with a strong form of hybrid logic. William Farmer’s system is a version of Church’s theory of types which allows terms to be non-denoting; hybrid logic is a version of modal logic in which it is possible to name worlds and evaluate expressions with respect to particular worlds. We motivate this combination of ideas in the in…Read more
-
8Malinowski modalization, modalization through fibring and the Leibniz hierarchyLogic Journal of the IGPL 21 (5): 836-852. 2013.
-
61A Coalgebraic Perspective on Logical InterpretationsStudia Logica 101 (4): 783-825. 2013.In Computer Science stepwise refinement of algebraic specifications is a well-known formal methodology for rigorous program development. This paper illustrates how techniques from Algebraic Logic, in particular that of interpretation, understood as a multifunction that preserves and reflects logical consequence, capture a number of relevant transformations in the context of software design, reuse, and adaptation, difficult to deal with in classical approaches. Examples include data encapsulation…Read more
-
3Relating Kleene Algebras with Pseudo UninormsIn Carlos Areces & Diana Costa (eds.), Dynamic Logic. New Trends and Applications: 4th International Workshop, DaLí 2022, Haifa, Israel, July 31–August 1, 2022, Revised Selected Papers, Springer Verlag. pp. 37-55. 2023.This paper explores a strict relation between two core notions of the semantics of programs and of fuzzy logics: Kleene Algebras and (pseudo) uninorms. It shows that every Kleene algebra induces a pseudo uninorm, and that some pseudo uninorms induce Kleene algebras. This connection establishes a new perspective on the theory of Kleene algebras and provides a way to build (new) Kleene algebras. The latter aspect is potentially useful as a source of formalism to capture and model programs acting w…Read more
-
13Completeness in Equational Hybrid Propositional Type TheoryStudia Logica 107 (6): 1159-1198. 2019.Equational hybrid propositional type theory ) is a combination of propositional type theory, equational logic and hybrid modal logic. The structures used to interpret the language contain a hierarchy of propositional types, an algebra and a Kripke frame. The main result in this paper is the proof of completeness of a calculus specifically defined for this logic. The completeness proof is based on the three proofs Henkin published last century: Completeness in type theory, The completeness of the…Read more
-
21Completeness in Equational Hybrid Propositional Type TheoryStudia Logica 107 (6): 1159-1198. 2019.Equational hybrid propositional type theory ) is a combination of propositional type theory, equational logic and hybrid modal logic. The structures used to interpret the language contain a hierarchy of propositional types, an algebra and a Kripke frame. The main result in this paper is the proof of completeness of a calculus specifically defined for this logic. The completeness proof is based on the three proofs Henkin published last century: Completeness in type theory, The completeness of the…Read more
-
21A Hilbert-Style Axiomatisation for Equational Hybrid LogicJournal of Logic, Language and Information 23 (1): 31-52. 2014.This paper introduces an axiomatisation for equational hybrid logic based on previous axiomatizations and natural deduction systems for propositional and first-order hybrid logic. Its soundness and completeness is discussed. This work is part of a broader research project on the development a general proof calculus for hybrid logics.
-
115Behavioral Algebraization of LogicsStudia Logica 91 (1): 63-111. 2009.We introduce and study a new approach to the theory of abstract algebraic logic (AAL) that explores the use of many-sorted behavioral logic in the role traditionally played by unsorted equational logic. Our aim is to extend the range of applicability of AAL toward providing a meaningful algebraic counterpart also to logics with a many-sorted language, and possibly including non-truth-functional connectives. The proposed behavioral approach covers logics which are not algebraizable according to t…Read more
-
13Behavioral equivalence of hidden k -logics: An abstract algebraic approachJournal of Applied Logic 16 72-91. 2016.