@inproceedings{63540e16e80b41c88f43120b9bd68ed6,
title = "Herbrand-confluence for cut elimination in classical first order logic",
abstract = "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.",
keywords = "First-order logic, Proof theory, Semantics of proofs, Term rewriting, Tree languages",
author = "Stefan Hetzl and Lutz Stra{\ss}burger",
year = "2012",
month = dec,
day = "1",
doi = "10.4230/LIPIcs.CSL.2012.320",
language = "English",
isbn = "9783939897422",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
pages = "320--334",
booktitle = "Computer Science Logic 2012 - 26th International Workshop/21th Annual Conference of the EACSL, CSL 2012",
note = "26th International Workshop on Computer Science Logic, CSL 2012/21st Annual Conference of the European Association for Computer Science Logic, EACSL ; Conference date: 03-09-2012 Through 06-09-2012",
}