Related papers: Unified Correspondence as a Proof-Theoretic Tool
Analytic proof calculi are introduced for box and diamond fragments of basic modal fuzzy logics that combine the Kripke semantics of modal logic K with the many-valued semantics of G\"odel logic. The calculi are used to establish…
We introduce proper display calculi for basic monotonic modal logic, the conditional logic CK and a number of their axiomatic extensions. These calculi are sound, complete, conservative and enjoy cut elimination and subformula property. Our…
We solve two problems in the theory of correspondences that have important implications in the theory of product systems. The first problem is the question whether every correspondence is the correspondence associated (by the representation…
In recent years the umbral calculus has emerged from the shadows to provide an elegant correspondence framework that automatically gives systematic solutions of ubiquitous difference equations --- discretized versions of the differential…
Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for…
Non-classical generalizations of classical modal logic have been developed in the contexts of constructive mathematics and natural language semantics. In this paper, we discuss a general approach to the semantics of non-classical modal…
The goal of this paper is to present an algebraic approach to the basic results of the theory of linear recurrence relations. This approach is based on the ideas from the theory of representations of one endomorphisms (a special case of…
Qualitative reasoning involves expressing and deriving knowledge based on qualitative terms such as natural language expressions, rather than strict mathematical quantities. Well over 40 qualitative calculi have been proposed so far, mostly…
This paper explores proof-theoretic aspects of hybrid type-logical grammars , a logic combining Lambek grammars with lambda grammars. We prove some basic properties of the calculus, such as normalisation and the subformula property and also…
This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic…
Kleene algebra with tests is an extension of Kleene algebra, the algebra of regular expressions, which can be used to reason about programs. We develop a coalgebraic theory of Kleene algebra with tests, along the lines of the coalgebraic…
A grammar logic refers to an extension to the multi-modal logic K in which the modal axioms are generated from a formal grammar. We consider a proof theory, in nested sequent calculus, of grammar logics with converse, i.e., every modal…
In this survey, we present in a unified way the categorical and syntactical settings of coherent differentiation introduced recently, which shows that the basic ideas of differential linear logic and of the differential lambda-calculus are…
The Ambient Logic (AL) has been proposed for expressing properties of process mobility in the calculus of Mobile Ambients (MA), and as a basis for query languages on semistructured data. In this paper, we study the expressiveness of AL. We…
We introduce proper display calculi for intuitionistic, bi-intuitionistic and classical linear logics with exponentials, which are sound, complete, conservative, and enjoy cut-elimination and subformula property. Based on the same design,…
We consider an extension of bi-intuitionistic logic with the traditional modalities from tense logic Kt. Proof theoretically, this extension is obtained simply by extending an existing sequent calculus for bi-intuitionistic logic with…
In previous works, a tableau calculus has been defined, which constitutes a decision procedure for hybrid logic with the converse and global modalities and a restricted use of the binder. This work shows how to extend such a calculus to…
Integral calculus on the space of gauge equivalent connections is developed. Loops, knots, links and graphs feature prominently in this description. The framework is well--suited for quantization of diffeomorphism invariant theories of…
The uniform one-dimensional fragment of first-order logic, U1, is a formalism that extends two-variable logic in a natural way to contexts with relations of all arities. We survey properties of U1 and investigate its relationship to…
We introduce a proper multi-type display calculus for bilattice logic (with conflation) for which we prove soundness, completeness, conservativity, standard subformula property and cut-elimination. Our proposal builds on the product…