A family of Gödel hybrid logics

In this paper, we define a family of fuzzy hybrid logics that are based on Gödel logic. It is composed of two infinite-valued versions called ${\mathsf{GH}}_{\infty }$ and ${\mathsf{WGH}}_{\infty }$, and a sequence of finitary valued versions ${({\mathsf{GH}}_n)}_{0<n<\infty }$. We define decision procedures for both ${\mathsf{WGH}}_{\infty }$ and ${({\mathsf{GH}}_n)}_{0<n<\infty }$ that are based on particular sequents and on a set of proof rules dealing with such sequents. As these rules are strongly invertible the procedures naturally allow one to generate countermodels. Therefore we prove the decidability and the finite model property for these logics. Finally, from the decision procedure of ${\mathsf{WGH}}_{\infty }$, we design a sound and complete sequent calculus for this logic.     

Coinductive models and normal forms for modal logics (or how we learned to stop worrying and love coinduction)

We present a coinductive definition of models for modal logics and show that it provides a homogeneous framework in which it is possible to include different modal languages ranging from classical modalities to operators from hybrid and memory logics. Moreover, results that had to be proved separately for each different language—but whose proofs were known to be mere routine—now can be proved in a general way. We show, for example, that we can have a unique definition of bisimulation for all these languages, and prove a single invariance-under-bisimulation theorem.We then use the new framework to investigate normal forms for modal logics. The normal form we introduce may have a smaller modal depth than the original formula, and it is inspired by global modalities like the universal modality and the satisfiability operator from hybrid logics. These modalities can be extracted from under the scope of other operators. We provide a general definition of extractable modalities and show how to compute extracted normal forms. As it is the case with other classical normal forms—e.g., the conjunctive normal form of propositional logic—the extracted normal form of a formula can be exponentially bigger than the original formula, if we require the two formulas to be equivalent. If we only require equi-satisfiability, then every modal formula has an extracted normal form which is only polynomially bigger than the original formula, and it can be computed in polynomial time.     

Interpolation and Amalgamation; Pushing the Limits. Part II

This is the second part of the paper [Part I] which appeared in the previous issue of this journal.     

The Concurrent,Continuous Fluent Calculus

The Fluent Calculus belongs to the established predicate calculus formalisms for reasoning about actions. Its underlying concept of state update axioms provides a solution to the basic representational and inferential Frame Problems in pure first-order logic. Extending a recent research result, we present a Fluent Calculus to reason about domains involving continuous change and where actions occur concurrently.     

Coherence in Substructural Categories

It is proved that MacLane's coherence results for monoidal and symmetric monoidal categories can be extended to some other categories with multiplication; namely, to relevant, affine and cartesian categories. All results are formulated in terms of natural transformations equipped with graphs (g-natural transformations) and corresponding morphism theorems are given as consequences. Using these results, some basic relations between the free categories of these classes are obtained.     

Correspondence Results for Relational Proof Systems with Application to the Lambek Calculus

We present a general framework for proof systems for relational theories. We discuss principles of the construction of deduction rules and correspondences reflecting relationships between semantics of relational logics and the rules of the respective proof systems. We illustrate the methods developed in the paper with examples relevant for the Lambek calculus and some of its extensions.     

An O(n log n)-Space Decision Procedure for the Relevance Logic B+

In previous work we gave a new proof-theoretical method for establishing upper-bounds on the space complexity of the provability problem of modal and other propositional non-classical logics. Here we extend and refine these results to give an O(n log n)-space decision procedure for the basic positive relevance logic B⁺. We compute this upper-bound by first giving a sound and complete, cut-free, labelled sequent system for B⁺, and then establishing bounds on the application of the rules of this system.     

First-order Expressivity for S5-models: Modal vs. Two-sorted Languages

Standard models for model predicate logic consist of a Kripke frame whose worlds come equipped with relational structures. Both modal and two-sorted predicate logic are natural languages for speaking about such models. In this paper we compare their expressivity. We determine a fragment of the two-sorted language for which the modal language is expressively complete on S5-models. Decidable criteria for modal definability are presented.