Document

**Published in:** LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs with prenex Pi_1-cuts in classical first-order logic corresponds to computing the language of a particular type of tree grammars. The present paper extends this connection to arbitrary (i.e. non-prenex) cuts without quantifier alternations. The key to treating non-prenex cuts lies in using a new class of tree grammars, constraint grammars, which describe the relationship of the applicability of its productions by a propositional formula.

Stefan Hetzl and Sebastian Zivota. Tree Grammars for the Elimination of Non-prenex Cuts. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 110-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{hetzl_et_al:LIPIcs.CSL.2015.110, author = {Hetzl, Stefan and Zivota, Sebastian}, title = {{Tree Grammars for the Elimination of Non-prenex Cuts}}, booktitle = {24th EACSL Annual Conference on Computer Science Logic (CSL 2015)}, pages = {110--127}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-90-3}, ISSN = {1868-8969}, year = {2015}, volume = {41}, editor = {Kreutzer, Stephan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.110}, URN = {urn:nbn:de:0030-drops-54103}, doi = {10.4230/LIPIcs.CSL.2015.110}, annote = {Keywords: proof theory, cut-elimination, Herbrand's theorem, tree grammars} }

Document

**Published in:** LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)

Recently a new connection between proof theory and formal language theory was introduced. It was shown that the operation of cut elimination for proofs in first-order predicate logic involving Pi_1-cuts corresponds to computing the language of a particular class of regular tree grammars. The present paper expands this connection to the level of Pi_2-cuts. Given a proof pi of a Sigma_1 formula with cuts only on Pi_2 formulæ, we show there is associated to pi a natural context-free tree grammar whose language is finite and yields a Herbrand disjunction for pi.

Bahareh Afshari, Stefan Hetzl, and Graham E. Leigh. Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{afshari_et_al:LIPIcs.TLCA.2015.1, author = {Afshari, Bahareh and Hetzl, Stefan and Leigh, Graham E.}, title = {{Herbrand Disjunctions, Cut Elimination and Context-Free Tree Grammars}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {1--16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.1}, URN = {urn:nbn:de:0030-drops-51516}, doi = {10.4230/LIPIcs.TLCA.2015.1}, annote = {Keywords: Classical logic, Context-free grammars, Cut elimination, First-order logic, Herbrand's theorem, Proof theory} }

Document

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

The sequent calculus is often criticized for requiring proofs to
contain large amounts of low-level syntactic details that can obscure the essence of a given proof. Because each inference rule introduces only a single connective, sequent proofs can separate closely related steps-such as instantiating a block of quantifiers-by irrelevant noise. Moreover, the sequential nature of sequent proofs forces proof steps that are syntactically non-interfering and permutable to nevertheless be written in some arbitrary order. The sequent calculus thus lacks a notion of canonicity: proofs that should be considered essentially the same may not have a common syntactic form. To fix this problem, many researchers have proposed replacing the sequent calculus with proof structures that are more parallel or geometric. Proof-nets, matings, and atomic flows are examples of such revolutionary formalisms. We propose, instead, an evolutionary approach to recover canonicity within the sequent calculus, which we illustrate for classical first-order logic. The essential element of our approach is the use of a multi-focused sequent calculus as the means of abstracting away the details from classical cut-free sequent proofs. We show that, among the multi-focused proofs, the maximally multi-focused proofs that make the foci as parallel as possible are canonical. Moreover, such proofs are isomorphic to expansion proofs - a well known, minimalistic, and parallel generalization of Herbrand
disjunctions - for classical first-order logic. This technique is a
systematic way to recover the desired essence of any sequent proof
without abandoning the sequent calculus.

Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 183-197, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{chaudhuri_et_al:LIPIcs.CSL.2012.183, author = {Chaudhuri, Kaustuv and Hetzl, Stefan and Miller, Dale}, title = {{A Systematic Approach to Canonicity in the Classical Sequent Calculus}}, booktitle = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL}, pages = {183--197}, 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.183}, URN = {urn:nbn:de:0030-drops-36723}, doi = {10.4230/LIPIcs.CSL.2012.183}, annote = {Keywords: Sequent Calculus, Canonicity, Classical Logic, Expansion Trees} }

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} }

X

Feedback for Dagstuhl Publishing

Feedback submitted

Please try again later or send an E-mail