Author name cluster

Lutz Straßburger

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

13 papers

2 author rows

FSCD Conference 2022 Conference Paper

A Graphical Proof Theory of Logical Time

Matteo Acclavio
Ross Horne
Sjouke Mauw
Lutz Straßburger

Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV.

Details

CSL Conference 2022 Conference Paper

BV and Pomset Logic Are Not the Same

Lê Thành Dung Nguyên
Lutz Straßburger

BV and pomset logic are two logics that both conservatively extend unit-free multiplicative linear logic by a third binary connective, which (i) is non-commutative, (ii) is self-dual, and (iii) lies between the "par" and the "tensor". It was conjectured early on (more than 20 years ago), that these two logics, that share the same language, that both admit cut elimination, and whose connectives have essentially the same properties, are in fact the same. In this paper we show that this is not the case. We present a formula that is provable in pomset logic but not in BV.

Details

FSCD Conference 2022 Conference Paper

Normalization Without Syntax

Willem Heijltjes
Dominic J. D. Hughes
Lutz Straßburger

We present normalization for intuitionistic combinatorial proofs (ICPs) and relate it to the simply-typed lambda-calculus. We prove confluence and strong normalization. Combinatorial proofs, or "proofs without syntax", form a graphical semantics of proof in various logics that is canonical yet complexity-aware: they are a polynomial-sized representation of sequent proofs that factors out exactly the non-duplicating permutations. Our approach to normalization aligns with these characteristics: it is canonical (free of permutations) and generic (readily applied to other logics). Our reduction mechanism is a canonical representation of reduction in sequent calculus with closed cuts (no abstraction is allowed below a cut), and relates to closed reduction in lambda-calculus and supercombinators. While we will use ICPs concretely, the notion of reduction is completely abstract, and can be specialized to give a reduction mechanism for any representation of typed normal forms.

Details

FLAP Journal 2021 Journal Article

Justification Logic for Constructive Modal Logic.

Roman Kuznets
Sonia Marin
Lutz Straßburger

We provide a treatment of the intuitionistic 3 modality in the style of justification logic. We introduce a new type of terms, called satisfiers, that justify consistency, obtain justification analogs for the constructive modal logics CK, CD, CT, and CS4, and prove the realization theorem for them.

Details

TCS Journal 2019 Journal Article

On the decision problem for MELL

Lutz Straßburger

In this short paper I will exhibit several mistakes in the recent attempt by Bimbó [3] to prove the decidability of the multiplicative exponential fragment of linear logic ( MELL ). In fact, the main mistake is so serious that there is no obvious fix, and therefore the decidability of MELL remains an open problem. As a side effect, this paper contains a complete (syntactic) proof of the decidability of the relevant version of MELL (called RMELL in this paper), that is the logic obtained from MELL by replacing the linear logic contraction rule by a general unrestricted version of the contraction rule. This proof can also be found (with a small error) in [3], and a semantic proof can be found in [35].

Details DOI

CSL Conference 2012 Conference Paper

Herbrand-Confluence for Cut Elimination in Classical First Order Logic

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 which witnesses they choose for which quantifiers, or in other words: we only consider the Herbrand-disjunction of a cut-free proof. Our main theorem is a confluence result for a natural class of proofs: all (possibly infinitely many) normal forms of the non-erasing reduction lead to the same Herbrand-disjunction.

Details

CSL Conference 2011 Conference Paper

The Focused Calculus of Structures

Kaustuv Chaudhuri
Nicolas Guenot
Lutz Straßburger

The focusing theorem identifies a complete class of sequent proofs that have no inessential non-deterministic choices and restrict the essential choices to a particular normal form. Focused proofs are therefore well suited both for the search and for the representation of sequent proofs. The calculus of structures is a proof formalism that allows rules to be applied deep inside a formula. Through this freedom it can be used to give analytic proof systems for a wider variety of logics than the sequent calculus, but standard presentations of this calculus are too permissive, allowing too many proofs. In order to make it more amenable to proof search, we transplant the focusing theorem from the sequent calculus to the calculus of structures. The key technical contribution is an incremental treatment of focusing that avoids trivializing the calculus of structures. We give a direct inductive proof of the completeness of the focused calculus of structures with respect to a more standard unfocused form. We also show that any focused sequent proof can be represented in the focused calculus of structures, and, conversely, any proof in the focused calculus of structures corresponds to a focused sequent proof.

Details

CSL Conference 2009 Conference Paper

Expanding the Realm of Systematic Proof Theory

Agata Ciabattoni
Lutz Straßburger
Kazushige Terui

Abstract This paper is part of a general project of developing a systematic and algebraic proof theory for nonclassical logics. Generalizing our previous work on intuitionistic-substructural axioms and single-conclusion (hyper)sequent calculi, we define a hierarchy on Hilbert axioms in the language of classical linear logic without exponentials. We then give a systematic procedure to transform axioms up to the level \({\mathcal P}_3'\) of the hierarchy into inference rules in multiple-conclusion (hyper)sequent calculi, which enjoy cut-elimination under a certain condition. This allows a systematic treatment of logics which could not be dealt with in the previous approach. Our method also works as a heuristic principle for finding appropriate rules for axioms located at levels higher than \({\mathcal P}_3'\). The case study of Abelian and Łukasiewicz logic is outlined.

Details

CSL Conference 2004 Conference Paper

On Proof Nets for Multiplicative Linear Logic with Units

Lutz Straßburger
François Lamarche

Abstract In 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 subtrees. These trees will be identified according to an equivalence relation based on a simple form of graph rewriting. We show the standard results of sequentialization and strong normalization of cut elimination. Furthermore, the identifications enforced on proofs are such that the proof nets, as they are presented here, form the arrows of the free (symmetric) *-autonomous category.

Details

TCS Journal 2003 Journal Article

MELL in the calculus of structures

Lutz Straßburger

The calculus of structures is a new proof theoretical formalism, like natural deduction, the sequent calculus and proof nets, for specifying logical systems syntactically. In a rule in the calculus of structures, the premise as well as the conclusion are structures, which are expressions that share properties of formulae and sequents. In this paper, I study a system for MELL, the multiplicative exponential fragment of linear logic, in the calculus of structures. It has the following features: a local promotion rule, no non-deterministic splitting of the context in the times rule and a modular proof for the cut elimination theorem. Further, derivations have a new property, called decomposition, that cannot be observed in any other known proof theoretical formalism.

Details DOI

LPAR Conference 2002 Conference Paper

A Local System for Linear Logic

Lutz Straßburger

Abstract In this paper I will present a deductive system for linear logic, in which all rules are local. In particular, the contraction rule is reduced to an atomic version, and there is no global promotion rule. In order to achieve this, it is necessary to depart from the sequent calculus and use the calculus of structures, which is a generalization of the one-sided sequent calculus. In a rule, premise and conclusion are not sequents, but structures, which are expressions that share properties of formulae and sequents.

Details

LPAR Conference 2002 Conference Paper

A Non-commutative Extension of MELL

Alessio Guglielmi
Lutz Straßburger

Abstract We extend multiplicative exponential linear logic (M EL)L by a non-commutative, self-dual logical operator. The extended system, called NEL is defined in the formalism of the calculus of structures, which is a generalisation of the sequent calculus and provides a more refined analysis of proofs. We should then be able to extend the range of applications of M E L, L by modelling a broad notion of sequentiality and providing new properties of proofs. We show some proof theoretical results: decomposition and cut elimination. The new operator represents a significant challenge: to get our results we use here for the first time some novel techniques, which constitute a uniform and modular approach to cut elimination, contrary to what is possible in the sequent calculus.

Details

CSL Conference 2001 Conference Paper

Non-commutativity and MELL in the Calculus of Structures

Alessio Guglielmi
Lutz Straßburger

Abstract We introduce the calculus of structures: it is more general than the sequent calculus and it allows for cut elimination and the subformula property. We show a simple extension of multiplicative linear logic, by a self-dual non-commutative operator inspired by CCS, that seems not to be expressible in the sequent calculus. Then we show that multiplicative exponential linear logic benefits from its presentation in the calculus of structures, especially because we can replace the ordinary, global promotion rule by a local version. These formal systems, for which we prove cut elimination, outline a range of techniques and properties that were not previously available. Contrarily to what happens in the sequent calculus, the cut elimination proof is modular.

Details