The present paper establishes systematic connections among the first-order correspondents of Sahlqvist modal reduction principles in various relational semantic settings, including crisp and many-valued Kripke frames, and crisp and many-valued polarity-based frames (aka enriched formal contexts). Building on unified correspondence theory, we aim at introducing a theoretical environment which makes it possible to: (a) compare and inter-relate the various frame correspondents (in different relational settings) of any given Sahlqvist modal reduction principle; (b) recognize when first-order sentences in the frame-correspondence languages of different types of relational structures encode the same “modal content”; (c) meaningfully transfer and represent well known relational properties such as reflexivity, transitivity, symmetry, seriality, confluence, density, across different semantic contexts. These results can be understood as a first step in a research program aimed at making correspondence theory not just (methodologically) unified, but also (effectively) parametric.

Temporal reasoning based on intervals is nowadays ubiquitous in artificial intelligence, and the most representative interval temporal logic, called HS, was introduced by Halpern and Shoham in the eighties. There has been a great effort in the past in studying the expressive power and computational properties of the satisfiability problem for HS and its fragments, but only recently HS has been proposed as a suitable formalism for artificial intelligence applications. Such applications highlighted some of the intrinsic limits of HS: Sometimes, when dealing with real-life data one is not able to express temporal relations and propositional labels in a definite, crisp way. In this paper, following the seminal ideas of Fitting and Zadeh, among others, we present a fuzzy generalization of HS that partially solves such problems of expressive power, and we prove that, as in the crisp case, its satisfiability problem is generally undecidable.

In recent years, unified correspondence has been developed as a generalized Sahlqvist theory which applies uniformly to all signatures of normal and regular (distributive) lattice expansions. This includes a general definition of the Sahlqvist and inductive formulas and inequalities in every such signature, based on order theory. This definition covers in particular all (bi-)intuitionistic modal logics. The theory of these logics has been intensively studied over the past seventy years in connection with classical polyadic modal logics, using suitable versions of Goedel-McKinsey-Tarski translations as main tools. It is therefore natural to ask (1) whether a general perspective on Goedel-McKinsey-Tarski translations can be attained, also based on order-theoretic principles like those underlying the general definition of Sahlqvist and inductive formulas and inequalities, which accounts for the known Goedel-McKinsey-Tarski translations and applies uniformly to all signatures of normal (distributive) lattice expansions; (2) whether this general perspective can be used to transfer correspondence and canonicity theorems for Sahlqvist and inductive formulas and inequalities in all signatures described above under Goedel-McKinsey-Tarski translations. In the present paper, we set out to answer these questions. We answer (1) in the affirmative; as to (2), we prove the transfer of the correspondence theorem for inductive inequalities of arbitrary signatures of normal distributive lattice expansions. We also prove the transfer of canonicity for inductive inequalities, but only restricted to arbitrary normal modal expansions of bi-intuitionistic logic. We also analyze the difficulties involved in obtaining the transfer of canonicity outside this setting, and indicate a route to extend the transfer of canonicity to all signatures of normal distributive lattice expansions.

The present article contributes to the development of the mathematical theory of epistemic updates using the tools of duality theory. Here, we focus on Probabilistic Dynamic Epistemic Logic (PDEL). We dually characterize the product update construction of PDEL-models as a certain construction transforming the complex algebras associated with the given model into the complex algebra associated with the updated model. Thanks to this construction, an interpretation of the language of PDEL can be defined on algebraic models based on Heyting algebras. This justifies our proposal for the axiomatization of the intuitionistic counterpart of PDEL.

There are two natural and well-studied approaches to temporal ontology and reasoning: point-based and interval-based. Usually, interval-based temporal reasoning deals with points as a particular case of duration-less intervals. A recent result by Balbiani, Goranko, and Sciavicco presented an explicit two-sorted point-interval temporal framework in which time instants (points) and time periods (intervals) are considered on a par, allowing the perspective to shift between these within the formal discourse. We consider here two-sorted first-order languages based on the same principle, and therefore including relations, as first studied by Reich, among others, between points, between intervals, and inter-sort. We give complete classifications of its sub-languages in terms of relative expressive power, thus determining how many, and which, are the intrinsically different extensions of two-sorted first-order logic with one or more such relations. This approach roots out the classical problem of whether or not points should be included in a interval-based semantics.

We investigate the canonicity of inequalities of the intuitionistic mu-calculus. The notion of canonicity in the presence of fixed point operators is not entirely straightforward. In the algebraic setting of canonical extensions we examine both the usual notion of canonicity and what we will call tame canonicity. This latter concept has previously been investigated for the classical mu-calculus by Bezhanishvili and Hodkinson. Our approach is in the spirit of Sahlqvist theory. That is, we identify syntactically-defined classes of inequalities, namely the restricted inductive and tame inductive inequalities, which are, respectively, canonical or tame canonical. Our approach is to use an algorithm which processes inequalities with the aim of eliminating propositional variables. The algorithm we introduce is closely related to the algorithms ALBA and mu-ALBA studied by Conradie, Palmigiano, et al. It is based on a calculus of rewrite rules, the soundness of which rests upon the way in which algebras embed into their canonical extensions and the order-theoretic properties of the latter. We show that the algorithm succeeds on every restricted inductive inequality by means of a so-called proper run, and that this is sufficient to guarantee their canonicity. Likewise, we are able to show that the algorithm succeeds on every tame inductive inequality by means of a so-called tame run. In turn, this guarantees their tame canonicity.

Journal Article On Sahlqvist theory for hybrid logics Get access Willem Conradie, Willem Conradie Search for other works by this author on: Oxford Academic Google Scholar Claudette Robinson Claudette Robinson Search for other works by this author on: Oxford Academic Google Scholar Journal of Logic and Computation, Volume 27, Issue 3, April 2017, Pages 867–900, https://doi.org/10.1093/logcom/exv045 Published: 23 July 2015 Article history Received: 08 November 2014 Published: 23 July 2015

There are two natural and well-studied approaches to temporal ontology and reasoning, that is, point-based and interval-based. Usually, interval-based temporal reasoning deals with points as a particular case of duration-less intervals. Recently, a two-sorted point-interval temporal logic in a modal framework in which time instants (points) and time periods (intervals) are considered on a par has been presented. We consider here two-sorted first-order languages, interpreted in the class of all linear orders, based on the same principle, with relations between points, between intervals, and inter-sort. First, for those languages containing only interval-interval, and only inter-sort relations we give complete classifications of their sub-fragments in terms of relative expressive power, determining how many, and which, are the different two-sorted first-order languages with one or more such relations. Then, we consider the full two-sorted first-order logic with all the above mentioned relations, restricting ourselves to identify all expressively complete fragments and all maximal expressively incomplete fragments, and posing the basis for a forthcoming complete classification.

Modal formulae express monadic second-order properties on Kripke frames, but in many important cases these have first-order equivalents. Computing such equivalents is important for both logical and computational reasons. On the other hand, canonicity of modal formulae is important, too, because it implies frame-completeness of logics axiomatized with canonical formulae. Computing a first-order equivalent of a modal formula amounts to elimination of second-order quantifiers. Two algorithms have been developed for second-order quantifier elimination: SCAN, based on constraint resolution, and DLS, based on a logical equivalence established by Ackermann. In this paper we introduce a new algorithm, SQEMA, for computing first-order equivalents (using a modal version of Ackermann's lemma) and, moreover, for proving canonicity of modal formulae. Unlike SCAN and DLS, it works directly on modal formulae, thus avoiding Skolemization and the subsequent problem of unskolemization. We present the core algorithm and illustrate it with some examples. We then prove its correctness and the canonicity of all formulae on which the algorithm succeeds. We show that it succeeds not only on all Sahlqvist formulae, but also on the larger class of inductive formulae, introduced in our earlier papers. Thus, we develop a purely algorithmic approach to proving canonical completeness in modal logic and, in particular, establish one of the most general completeness results in modal logic so far.

In Conradie, Goranko, and Vakarelov (2006, Logical Methods in Computer Science, 2) we introduced a new algorithm, ⁠, for computing first-order equivalents and proving the canonicity of modal formulae of the basic modal language. Here we extend ⁠, first to arbitrary and reversive polyadic modal languages, and then to hybrid polyadic languages too. We present the algorithm, illustrate it with some examples, and prove its correctness with respect to local equivalence of the input and output formulae, its completeness with respect to the polyadic inductive formulae introduced in Goranko and Vakarelov (2001, J. Logic. Comput., 11, 737–754) and Goranko and Vakarelov (2006, Ann. Pure. Appl. Logic, 141, 180–217), and the d-persistence (with respect to descriptive frames) of the formulae on which the algorithm succeeds. These results readily expand to completeness with respect to hybrid inductive polyadic formulae and di-persistence (with respect to discrete frames) in hybrid reversive polyadic languages.