Herbrand-Confluence for Cut Elimination in Classical First Order Logic

Stefan Hetzl 1 Lutz Straßburger 2, 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Type de document :
Communication dans un congrès
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

Contributeur : Lutz Straßburger <>
Soumis le : lundi 3 décembre 2012 - 11:36:27
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : samedi 17 décembre 2016 - 18:36:59


Fichiers produits par l'(les) auteur(s)




Stefan Hetzl, Lutz Straßburger. Herbrand-Confluence for Cut Elimination in Classical First Order Logic. CSL 2012, Sep 2012, Fontainebleau, France. 2012, 〈http://drops.dagstuhl.de/opus/volltexte/2012/3681/〉. 〈10.4230/LIPIcs.CSL.2012.320〉. 〈hal-00759228〉



Consultations de la notice


Téléchargements de fichiers