Document

**Published in:** LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

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.

Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Normalization Without Syntax. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 19:1-19:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{heijltjes_et_al:LIPIcs.FSCD.2022.19, author = {Heijltjes, Willem B. and Hughes, Dominic J. D. and Stra{\ss}burger, Lutz}, title = {{Normalization Without Syntax}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {19:1--19:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.19}, URN = {urn:nbn:de:0030-drops-163004}, doi = {10.4230/LIPIcs.FSCD.2022.19}, annote = {Keywords: combinatorial proofs, intuitionistic logic, lambda-calculus, Curry-Howard, proof nets} }

Document

**Published in:** LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)

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.

Matteo Acclavio, Ross Horne, Sjouke Mauw, and Lutz Straßburger. A Graphical Proof Theory of Logical Time. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 22:1-22:25, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{acclavio_et_al:LIPIcs.FSCD.2022.22, author = {Acclavio, Matteo and Horne, Ross and Mauw, Sjouke and Stra{\ss}burger, Lutz}, title = {{A Graphical Proof Theory of Logical Time}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {22:1--22:25}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-233-4}, ISSN = {1868-8969}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.22}, URN = {urn:nbn:de:0030-drops-163037}, doi = {10.4230/LIPIcs.FSCD.2022.22}, annote = {Keywords: proof theory, causality, deep inference} }

Document

**Published in:** LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

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.

Lê Thành Dũng (Tito) Nguyễn and Lutz Straßburger. BV and Pomset Logic Are Not the Same. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 32:1-32:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{nguyen_et_al:LIPIcs.CSL.2022.32, author = {Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng (Tito) and Stra{\ss}burger, Lutz}, title = {{BV and Pomset Logic Are Not the Same}}, booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)}, pages = {32:1--32:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-218-1}, ISSN = {1868-8969}, year = {2022}, volume = {216}, editor = {Manea, Florin and Simpson, Alex}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.32}, URN = {urn:nbn:de:0030-drops-157521}, doi = {10.4230/LIPIcs.CSL.2022.32}, annote = {Keywords: proof nets, deep inference, pomset logic, system BV, cographs, dicographs, series-parallel orders} }

Document

**Published in:** LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

We present canonical proof nets for first-order additive linear logic, the fragment of linear logic with sum, product, and first-order universal and existential quantification. We present two versions of our proof nets. One, witness nets, retains explicit witnessing information to existential quantification. For the other, unification nets, this information is absent but can be reconstructed through unification. Unification nets embody a central contribution of the paper: first-order witness information can be left implicit, and reconstructed as needed. Witness nets are canonical for first-order additive sequent calculus. Unification nets in addition factor out any inessential choice for existential witnesses. Both notions of proof net are defined through coalescence, an additive counterpart to multiplicative contractibility, and for witness nets an additional geometric correctness criterion is provided. Both capture sequent calculus cut-elimination as a one-step global composition operation.

Willem B. Heijltjes, Dominic J. D. Hughes, and Lutz Straßburger. Proof Nets for First-Order Additive Linear Logic. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 22:1-22:22, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{heijltjes_et_al:LIPIcs.FSCD.2019.22, author = {Heijltjes, Willem B. and Hughes, Dominic J. D. and Stra{\ss}burger, Lutz}, title = {{Proof Nets for First-Order Additive Linear Logic}}, booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}, pages = {22:1--22:22}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-107-8}, ISSN = {1868-8969}, year = {2019}, volume = {131}, editor = {Geuvers, Herman}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.22}, URN = {urn:nbn:de:0030-drops-105297}, doi = {10.4230/LIPIcs.FSCD.2019.22}, annote = {Keywords: linear logic, first-order logic, proof nets, Herbrand’s theorem} }

Document

**Published in:** LIPIcs, Volume 84, 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)

This paper introduces combinatorial flows that generalize combinatorial proofs such that they also include cut and substitution as methods of proof compression. We show a normalization procedure for combinatorial flows, and how syntactic proofs are translated into combinatorial flows and vice versa.

Lutz Straßburger. Combinatorial Flows and Their Normalisation. In 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 84, pp. 31:1-31:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{straburger:LIPIcs.FSCD.2017.31, author = {Stra{\ss}burger, Lutz}, title = {{Combinatorial Flows and Their Normalisation}}, booktitle = {2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)}, pages = {31:1--31:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-047-7}, ISSN = {1868-8969}, year = {2017}, volume = {84}, editor = {Miller, Dale}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2017.31}, URN = {urn:nbn:de:0030-drops-77204}, doi = {10.4230/LIPIcs.FSCD.2017.31}, annote = {Keywords: proof equivalence, cut elimination, substitution, deep inference} }

Document

**Published in:** LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

Focusing is a general technique for syntactically compartmentalizing
the non-deterministic choices in a proof system, which not only
improves proof search but also has the representational benefit of
distilling sequent proofs into synthetic normal forms. However, since
focusing is usually specified as a restriction of the sequent
calculus, the technique has not been transferred to logics that lack a
(shallow) sequent presentation, as is the case for some of the logics
of the modal cube. We have recently extended the focusing technique
to classical nested sequents, a generalization of ordinary sequents.
In this work we further extend focusing to intuitionistic nested
sequents, which can capture all the logics of the intuitionistic S5
cube in a modular fashion. We present an internal cut-elimination
procedure for the focused system which in turn is used to show its
completeness.

Kaustuv Chaudhuri, Sonia Marin, and Lutz Straßburger. Modular Focused Proof Systems for Intuitionistic Modal Logics. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 16:1-16:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{chaudhuri_et_al:LIPIcs.FSCD.2016.16, author = {Chaudhuri, Kaustuv and Marin, Sonia and Stra{\ss}burger, Lutz}, title = {{Modular Focused Proof Systems for Intuitionistic Modal Logics}}, booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)}, pages = {16:1--16:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-010-1}, ISSN = {1868-8969}, year = {2016}, volume = {52}, editor = {Kesner, Delia and Pientka, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.16}, URN = {urn:nbn:de:0030-drops-59947}, doi = {10.4230/LIPIcs.FSCD.2016.16}, annote = {Keywords: intuitionistic modal logic, focusing, proof search, cut elimination, nested sequents} }

Document

**Published in:** LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Recently it has been observed that the set of all sound linear inference rules in propositional logic is already coNP-complete, i.e. that every Boolean tautology can be written as a (left- and right-) linear rewrite rule. This raises the question of whether there is a rewriting system on linear terms of propositional logic that is sound and complete for the set of all such rewrite rules. We show in this paper that, as long as reduction steps are polynomial-time decidable, such a rewriting system does not exist unless coNP=NP.
We draw tools and concepts from term rewriting, Boolean function theory and graph theory in order to access the required intermediate results. At the same time we make several connections between these areas that, to our knowledge, have not yet been presented and constitute a rich theoretical framework for reasoning about linear TRSs for propositional logic.

Anupam Das and Lutz Straßburger. No complete linear term rewriting system for propositional logic. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 127-142, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{das_et_al:LIPIcs.RTA.2015.127, author = {Das, Anupam and Stra{\ss}burger, Lutz}, title = {{No complete linear term rewriting system for propositional logic}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {127--142}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-85-9}, ISSN = {1868-8969}, year = {2015}, volume = {36}, editor = {Fern\'{a}ndez, Maribel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.127}, URN = {urn:nbn:de:0030-drops-51935}, doi = {10.4230/LIPIcs.RTA.2015.127}, annote = {Keywords: Linear rules, Term rewriting, Propositional logic, Proof theory, Deep inference} }

Document

**Published in:** LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

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.

Stefan Hetzl and Lutz Straßburger. Herbrand-Confluence for Cut Elimination in Classical First Order Logic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 320-334, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{hetzl_et_al:LIPIcs.CSL.2012.320, author = {Hetzl, Stefan and Stra{\ss}burger, Lutz}, title = {{Herbrand-Confluence for Cut Elimination in Classical First Order Logic}}, booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL}, pages = {320--334}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-42-2}, ISSN = {1868-8969}, year = {2012}, volume = {16}, editor = {C\'{e}gielski, Patrick and Durand, Arnaud}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.320}, URN = {urn:nbn:de:0030-drops-36815}, doi = {10.4230/LIPIcs.CSL.2012.320}, annote = {Keywords: proof theory, first-order logic, tree languages, term rewriting, semantics of proofs} }

Document

**Published in:** LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

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.

Kaustuv Chaudhuri, Nicolas Guenot, and Lutz Straßburger. The Focused Calculus of Structures. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 159-173, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{chaudhuri_et_al:LIPIcs.CSL.2011.159, author = {Chaudhuri, Kaustuv and Guenot, Nicolas and Stra{\ss}burger, Lutz}, title = {{The Focused Calculus of Structures}}, booktitle = {Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL}, pages = {159--173}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-32-3}, ISSN = {1868-8969}, year = {2011}, volume = {12}, editor = {Bezem, Marc}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.159}, URN = {urn:nbn:de:0030-drops-32297}, doi = {10.4230/LIPIcs.CSL.2011.159}, annote = {Keywords: focusing, polarity, calculus of structures, linear logic} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail