Search

• < Previous
• 1
• Next >

---

A System of Interaction and Structure III: The Complexity of BV and Pomset Logic

Lê Thành Dũng Nguyên ; Lutz Straßburger.

Pomset logic and BV are both logics that extend multiplicative linear logic (with Mix) with a third connective that is self-dual and non-commutative. Whereas pomset logic originates from the study of coherence spaces and proof nets, BV originates from the study of series-parallel orders, cographs,&nbsp;[&hellip;]

---

Herbrand-Confluence

Stefan Hetzl ; Lutz Straßburger.

We consider cut-elimination in the sequent calculus for classical first-order logic. It is well known that this system, in its most general form, is neither confluent nor strongly normalizing. In this work we take a coarser (and mathematically more realistic) look at cut-free proofs. We analyze&nbsp;[&hellip;]

---

On linear rewriting systems for Boolean logic and some applications to proof theory

Anupam Das ; Lutz Straßburger.

Linear rules have played an increasing role in structural proof theory in recent years. It has been observed that the set of all sound linear inference rules in Boolean logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-)linear rewrite rule. In&nbsp;[&hellip;]

---

On Nested Sequents for Constructive Modal Logics

Lutz Strassburger ; Anupam Das ; Ryuta Arisaka.

We present deductive systems for various modal logics that can be obtained from the constructive variant of the normal modal logic CK by adding combinations of the axioms d, t, b, 4, and 5. This includes the constructive variants of the standard modal logics K4, S4, and S5. We use for our&nbsp;[&hellip;]

---

From Proof Nets to the Free *-Autonomous Category

Francois Lamarche ; Lutz Strassburger.

In the first part of this paper we present a theory of proof nets for full multiplicative linear logic, including the two units. It naturally extends the well-known theory of unit-free multiplicative proof nets. A linking is no longer a set of axiom links but a tree in which the axiom links are&nbsp;[&hellip;]

---

An Analytic Propositional Proof System on Graphs

Matteo Acclavio ; Ross Horne ; Lutz Straßburger.

In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas&nbsp;[&hellip;]

---