Behavioral Algebraization of Logics

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. Presented by Daniele Mundici     

On maximal intermediate predicate constructive logics

We extend to the predicate frame a previous characterization of the maximal intermediate propositional constructive logics. This provides a technique to get maximal intermediate predicate constructive logics starting from suitable sets of classically valid predicate formulae we call maximal nonstandard predicate constructive logics. As an example of this technique, we exhibit two maximal intermediate predicate constructive logics, yet leaving open the problem of stating whether the two logics are distinct. Further properties of these logics will be also investigated.Presented by H. Ono     

Proof-Theoretic Functional Completeness for the Hybrid Logics of Everywhere and Elsewhere

A hybrid logic is obtained by adding to an ordinary modal logic further expressive power in the form of a second sort of propositional symbols called nominals and by adding so-called satisfaction operators. In this paper we consider hybridized versions of S5 (“the logic of everywhere”) and the modal logic of inequality (“the logic of elsewhere”). We give natural deduction systems for the logics and we prove functional completeness results.     

Comparing Semantics of Logics for Multi-Agent Systems

We draw parallels between several closely related logics that combine — in different proportions — elements of game theory, computation tree logics, and epistemic logics to reason about agents and their abilities. These are: the coalition game logics CL and ECL introduced by Pauly 2000, the alternating-time temporal logic ATL developed by Alur, Henzinger and Kupferman between 1997 and 2002, and the alternating-time temporal epistemic logic ATEL by van der Hoek and Wooldridge (2002). In particular, we establish some subsumption and equivalence results for their semantics, as well as interpretation of the alternating-time temporal epistemic logic into ATL. The focus in this paper is on models: alternating transition systems, multi-player game models (alias concurrent game structures) and coalition effectivity models turn out to be intimately related, while alternating epistemic transition systems share much of their philosophical and formal apparatus. Our approach is constructive: we present ways to transform between different types of models and languages.     

On the Algebraizability of Annotated Logics

Annotated logics were introduced by V.S. Subrahmanian as logical foundations for computer programming. One of the difficulties of these systems from the logical point of view is that they are not structural, i.e., their consequence relations are not closed under substitutions. In this paper we give systems of annotated logics that are equivalent to those of Subrahmanian in the sense that everything provable in one type of system has a translation that is provable in the other. Moreover these new systems are structural. We prove that these systems are weakly congruential, namely, they have an infinite system of congruence 1-formulas. Moreover, we prove that an annotated logic is algebraizable (i.e., it has a finite system of congruence formulas,) if and only if the lattice of annotation constants is finite.     

On Modal Logics Characterized by Models with Relative Accessibility Relations: Part II

This work is divided in two papers (Part I and Part II). In Part I, we introduced the class of Rare-logics for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability were established by faithfully translating the Rare-logics into more standard modal logics (some of them contain the universal modal operator).In Part II, we push forward the results from Part I. For Rare-logics with nominals (present at the level of formulae and at the level of modal expressions), we show that the constructions from Part I can be extended although it is technically more involved. We also characterize a class of standard modal logics for which the universal modal operator can be eliminated as far as satifiability is concerned. Although the previous results have a semantic flavour, we are also able to define proof systems for Rare-logics from existing proof systems for the corresponding standard modal logics. Last, but not least, decidability results for Rare-logics are established uniformly, in particular for information logics derived from rough set theory.Since this paper is the continuation of Part I, we do not recall here the definitions of Part I although we refer to them.     

Selfextensional Logics with a Conjunction

A logic is selfextensional if its interderivability (or mutual consequence) relation is a congruence relation on the algebra of formulas. In the paper we characterize the selfextensional logics with a conjunction as the logics that can be defined using the semilattice order induced by the interpretation of the conjunction in the algebras of their algebraic counterpart. Using the charactrization we provide simpler proofs of several results on selfextensional logics with a conjunction obtained in [13] using Gentzen systems. We also obtain some results on Fregean logics with conjunction.This paper is a version of the invited talk at the conference Trends in Logic III, dedicated to the memory of A. MOSTOWSKI, H. RASIOWA and C. RRAUSZER, and held in Warsaw and Ruciane-Nida from 23rd to 25th September 2005.     

Natural Deduction for Non-Classical Logics

We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a base logic of labelled formulae, and a theory of labels characterizing the properties of the Kripke models. By appropriate combinations we capture both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. Our approach is modular and supports uniform proofs of soundness, completeness and proof normalization. We have implemented our work in the Isabelle Logical Framework.     

Action negation and alternative reductions for dynamic deontic logics

Dynamic deontic logics reduce normative assertions about explicit complex actions to standard dynamic logic assertions about the relation between complex actions and violation conditions. We address two general, but related problems in this field. The first is to find a formalization of the notion of ‘action negation’ that (1) has an intuitive interpretation as an action forming combinator and (2) does not impose restrictions on the use of other relevant action combinators such as sequence and iteration, and (3) has a meaningful interpretation in the normative context. The second problem we address concerns the reduction from deontic assertions to dynamic logic assertions. Our first point is that we want this reduction to obey the free-choice semantics for norms. For ought-to-be deontic logics it is generally accepted that the free-choice semantics is counter-intuitive. But for dynamic deontic logics we actually consider it a viable, if not, the better alternative. Our second concern with the reduction is that we want it to be more liberal than the ones that were proposed before in the literature. For instance, Meyer's reduction does not leave room for action whose normative status is neither permitted nor forbidden. We test the logics we define in this paper against a set of minimal logic requirements.     

Semantics for Dual and Symmetric Combinatory Calculi

We define dual and symmetric combinatory calculi (inequational and equational ones), and prove their consistency. Then, we introduce algebraic and set theoretical– relational and operational – semantics, and prove soundness and completeness. We analyze the relationship between these logics, and argue that inequational dual logics are the best suited to model computation.     

On Modal Logics Characterized by Models with Relative Accessibility Relations: Part I

This work is divided in two papers (Part I and Part II). In Part I, we study a class of polymodal logics (herein called the class of "Rare-logics") for which the set of terms indexing the modal operators are hierarchized in two levels: the set of Boolean terms and the set of terms built upon the set of Boolean terms. By investigating different algebraic properties satisfied by the models of the Rare-logics, reductions for decidability are established by faithfully translating the Rare-logics into more standard modal logics. The main idea of the translation consists in eliminating the Boolean terms by taking advantage of the components construction and in using various properties of the classes of semilattices involved in the semantics. The novelty of our approach allows us to prove new decidability results (presented in Part II), in particular for information logics derived from rough set theory and we open new perspectives to define proof systems for such logics (presented also in Part II).     

Two notions of compactness in Gödel logics

Compactness is an important property of classical propositional logic. It can be defined in two equivalent ways. The first one states that simultaneous satisfiability of an infinite set of formulae is equivalent to the satisfiability of all its finite subsets. The second one states that if a set of formulae entails a formula, then there is a finite subset entailing this formula as well.In propositional many-valued logic, we have different degrees of satisfiability and different possible definitions of entailment, hence the questions of compactness is more complex. In this paper we will deal with compactness of Gödel, Gödel_Δ, and Gödel_～ logics.There are several results (all for the countable set of propositional variables) concerning the compactness (based on satisfiability) of these logic by Cintula and Navara, and the question of compactness (based on entailment) for Gödel logic was fully answered by Baaz and Zach (see papers [3] and [2]).In this paper we give a nearly complete answer to the problem of compactness based on both concepts for all three logics and for an arbitrary cardinality of the set of propositional variables. Finally, we show a tight correspondence between these two concepts     

AN INTUITIONISTIC CHARACTERIZATION OF CLASSICAL LOGIC

By introducing the intensional mappings and their properties, we establish a new semantical approach of characterizing intermediate logics. First prove that this new approach provides a general method of characterizing and comparing logics without changing the semantical interpretation of implication connective. Then show that it is adequate to characterize all Kripke_complete intermediate logics by showing that each of these logics is sound and complete with respect to its (unique) ‘weakest characterization property’ of intensional mappings. In particular, we show that classical logic has the weakest characterization property , which is the strongest among all possible weakest characterization properties of intermediate logics. Finally, it follows from this result that a translation is an embedding of classical logic into intuitionistic logic, iff. its semantical counterpart has the property .      

A general tableau method for propositional interval temporal logics: Theory and implementation

In this paper, we focus our attention on tableau methods for propositional interval temporal logics. These logics provide a natural framework for representing and reasoning about temporal properties in several areas of computer science. However, while various tableau methods have been developed for linear and branching time point-based temporal logics, not much work has been done on tableau methods for interval-based ones. We develop a general tableau method for Venema's CDT logic interpreted over partial orders (BCDT⁺ for short). It combines features of the classical tableau method for first-order logic with those of explicit tableau methods for modal logics with constraint label management, and it can be easily tailored to most propositional interval temporal logics proposed in the literature. We prove its soundness and completeness, and we show how it has been implemented.     

Deontic action logic, atomic boolean algebras and fault-tolerance

We introduce a deontic action logic and its axiomatization. This logic has some useful properties (soundness, completeness, compactness and decidability), extending the properties usually associated with such logics. Though the propositional version of the logic is quite expressive, we augment it with temporal operators, and we outline an axiomatic system for this more expressive framework. An important characteristic of this deontic action logic is that we use boolean combinators on actions, and, because of finiteness restrictions, the generated boolean algebra is atomic, which is a crucial point in proving the completeness of the axiomatic system. As our main goal is to use this logic for reasoning about fault-tolerant systems, we provide a complete example of a simple application, with an attempt at formalization of some concepts usually associated with fault-tolerance.     

Unity in nominal equational reasoning: The algebra of equality on nominal sets

There are currently no fewer than four dedicated logics for equality reasoning over nominal sets: nominal algebra, nominal equational logic, nominal equational logic with equality only, and permissive-nominal algebra.In this survey and research paper we present these logics side-by-side in a common notation, survey their similarities and differences, discuss their proof- and model-theories, and discuss in detail what the implications of those differences are for mathematical reasoning in each of them.     

Complete Axiomatizations for Reasoning about Knowledge and Branching Time

Sound and complete axiomatizations are provided for a number of different logics involving modalities for the knowledge of multiple agents and operators for branching time, extending previous work of Halpern, van der Meyden and Vardi [to appear, SIAM Journal on Computing] for logics of knowledge and linear time. The paper considers the system constraints of synchrony, perfect recall and unique initial states, which give rise to interaction axioms. The language is based on the temporal logic CTL*, interpreted with respect to a version of the bundle semantics.     

A clausal resolution method for extended computation tree logic ECTL

A temporal clausal resolution method was originally developed for linear time temporal logic and further extended to the branching-time framework of Computation Tree Logic (CTL). In this paper, following our general idea to expand the applicability of this efficient method to more expressive formalisms useful in a variety of applications in computer science and AI requiring branching time logics, we define a clausal resolution technique for Extended Computation Tree Logic (ECTL). The branching-time temporal logic ECTL is strictly more expressive than CTL in allowing fairness operators. The key elements of the resolution method for ECTL, namely the clausal normal form, the concepts of step resolution and a temporal resolution, are introduced and justified with respect to this new framework. Although in developing these components we incorporate many of the techniques defined for CTL, we need novel mechanisms in order to capture fairness together with the limit closure property of the underlying tree models. We accompany our presentation of the relevant techniques by examples of the application of the temporal resolution method. Finally, we provide a correctness argument and consider future work discussing an extension of the method yet further, to the logic CTL^*, the most powerful logic of this class.     

Dialogue Games for Many-Valued Logics — an Overview

An overview of different versions and applications of Lorenzen’s dialogue game approach to the foundations of logic, here largely restricted to the realm of manyvalued logics, is presented. Among the reviewed concepts and results are Giles’s characterization of ?ukasiewicz logic and some of its generalizations to other fuzzy logics, including interval based logics, a parallel version of Lorenzen’s game for intuitionistic logic that is adequate for finite- and infinite-valued Gödel logics, and a truth comparison game for infinite-valued Gödel logic.