33 citations · 87 across the 15 of their papers we have counts for
15 papers
Interpolation via Generalized Splitting
Lutz Straßburger
We propose a new proof theoretical method for proving Lyndon interpolation. Our proof does not use the sequent calculus but is based on a generalization of the splitting lemma in d…
Proof Identity and Categorical Models of BV
Matteo Acclavio, Lutz Straßburger, Vladimir Zamdzhiev
BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-…
Where are the Teeth of the Fourth Power?
Lutz Straßburger
The news we consume influence our political opinions, and therefore whoever controls which news we read also controls our political opinions. Does this mean that the algorithms tha…
Coqlex: Generating Formally Verified Lexers
Wendlasida Ouedraogo, Gabriel Scherer, Lutz Strassburger
A compiler consists of a sequence of phases going from lexical analysis to code generation. Ideally, the formal verification of a compiler should include the formal verification of…
Intuitionistic S4 is decidable
Marianna Girlando, Roman Kuznets, Sonia Marin +2
In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years…
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 originate…
Combinatorial Proofs and Decomposition Theorems for First-order Logic
Dominic Hughes, Lutz Straßburger, Jui-Hsuan Wu
We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof sy…
Towards a Denotational Semantics for Proofs in Constructive Modal Logic
Matteo Acclavio, Davide Catta, Lutz Straßburger
In this paper we provide two new semantics for proofs in the constructive modal logics CK and CD. The first semantics is given by extending the syntax of combinatorial proofs for p…
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-co…
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 al…
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,…
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…
Proof Nets and the Identity of Proofs
Lutz Strassburger
These are the notes for a 5-lecture-course given at ESSLLI 2006 in Malaga, Spain. The URL of the school is http://esslli2006.lcc.uma.es/ . This version slightly differs from the on…
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-…
On the Axiomatisation of Boolean Categories with and without Medial
Lutz Strassburger
The term ``Boolean category'' should be used for describing an object that is to categories what a Boolean algebra is to posets. More specifically, a Boolean category should provid…