相关论文: A System of Interaction and Structure

We obtain, for the first time, a modular many-valued semantics for combined logics, which is built directly from many-valued semantics for the logics being combined, by means of suitable universal operations over partial non-deterministic…

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…

Intuitionistic logic extended with decidable propositional atoms combines classical properties in its propositional part and intuitionistic properties for derivable formulas not containing propositional symbols. Sequent calculus is used as…

Multiplicative linear logic is a very well studied formal system, and most such studies are concerned with the one-sided sequent calculus. In this paper we look in detail at existing translations between a deep inference system and the…

In this paper we explore the design of sequent calculi operating on graphs. For this purpose, we introduce a set of logical connectives allowing us to extend the correspondence between cographs and classical propositional formulas to any…

A quantitative model of concurrent interaction is introduced. The basic objects are linear combinations of partial order relations, acted upon by a group of permutations that represents potential non-determinism in synchronisation. This…

We present nested sequent systems for propositional G\"odel-Dummett logic and its first-order extensions with non-constant and constant domains, built atop nested calculi for intuitionistic logics. To obtain nested systems for these…

Development of a contraction-free BI sequent calculus, be it in the sense of G3i or G4i, has not been successful in literature. We address the open problem by presenting such a sequent system. In fact our calculus involves no structural…

Substructural logics are formal logical systems that omit familiar structural rules of classical and intuitionistic logic such as contraction, weakening, exchange (commutativity), and associativity. This leads to a resource-sensitive…

On the ground of a general theorem concerning the admissibility of the structural rules in sequent calculi with additional atomic rules, we develop a proof theoretic analysis for several extensions of the ${\bf G3[mic]}$ sequent calculi…

A term calculus for the proofs in multiplicative-additive linear logic is introduced and motivated as a programming language for channel based concurrency. The term calculus is proved complete for a semantics in linearly distributive…

We present a comprehensive programme analysing the decomposition of proof systems for non-classical logics into proof systems for other logics, especially classical logic, using an algebra of constraints. That is, one recovers a proof…

We introduce a logic for knowledge representation and reasoning on protein-protein interactions. Modulo a theory, formulas describe protein structures and dynamic changes. They can be composed in order to add or remove static and dynamic…

In this paper, we use a categorical and functorial set up to model the syntax and inference of logics with algebraic signature, extending previous works on algebraisation of logics. The main feature of this work is that structurality, or…

In this paper, we introduce a general family of sequent-style calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi \emph{constructive}, we show that any…

Logical bilateralism challenges traditional concepts of logic by treating assertion and denial as independent yet opposed acts. While initially devised to justify classical logic, its constructive variants show that both acts admit…

We apply to logic programming some recently emerging ideas from the field of reduction-based communicating systems, with the aim of giving evidence of the hidden interactions and the coordination mechanisms that rule the operational…

The work is devoted to Computability Logic (CoL) -- the philosophical/mathematical platform and long-term project for redeveloping classical logic after replacing truth} by computability in its underlying semantics (see…

We revisit the behavioral approach to systems theory and make explicit the abstract pattern that governs it. Our end goal is to use that pattern to understand interaction-related phenomena that emerge when systems interact. Rather than…

We introduce a framework that allows for the construction of sequent systems for expressive description logics extending ALC. Our framework not only covers a wide array of common description logics, but also allows for sequent systems to be…