Manuel Martins

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 the standard approach, while also bringing a new algebraic perspective to logics which are algebraizable using the standard tools of AAL. Furthermore, we pave the way toward a robust behavioral theory of AAL, namely by providing a behavioral version of the Leibniz operator which allows us to generalize the traditional Leibniz hierarchy, as well as several well-known characterization results. A number of meaningful examples will be used to illustrate the novelties and advantages of the approach.

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 and the decomposition of operations into atomic transactions. But if interpretations open such a new research avenue in program refinement, (conceptual) tools are needed to reason about them. In this line, the paper’s main contribution is a study of the correspondence between logical interpretations and morphisms of a particular kind of coalgebras. This opens way to the use of coalgebraic constructions, such as simulation and bisimulation, in the study of interpretations between (abstract) logics

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 first-order functional calculus and Completeness in propositional type theory. More precisely, from and we take the idea of building the model described by the maximal consistent set; in our case the maximal consistent set has to be named, \-saturated and extensionally algebraic-saturated due to the hybrid and equational nature of \. From, we use the result that any element in the hierarchy has a name. The challenge was to deal with all the heterogeneous components in an integrated system.

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 first-order functional calculus and Completeness in propositional type theory. More precisely, from and we take the idea of building the model described by the maximal consistent set; in our case the maximal consistent set has to be named, \-saturated and extensionally algebraic-saturated due to the hybrid and equational nature of \. From, we use the result that any element in the hierarchy has a name. The challenge was to deal with all the heterogeneous components in an integrated system.

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 introduction, and devote the rest of the article to defining, axiomatising, and proving a completeness result for $\mathcal {HPTT}$.

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 with fuzzy behaviours and domains.