Herbrand-Confluence for Cut Elimination in Classical First Order Logic - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2012

Herbrand-Confluence for Cut Elimination in Classical First Order Logic

Résumé

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.
Fichier principal
Vignette du fichier
HerbrandConfluence.pdf (541.2 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00759228 , version 1 (03-12-2012)

Identifiants

Citer

Stefan Hetzl, Lutz Strassburger. Herbrand-Confluence for Cut Elimination in Classical First Order Logic. CSL 2012, Sep 2012, Fontainebleau, France. ⟨10.4230/LIPIcs.CSL.2012.320⟩. ⟨hal-00759228⟩
208 Consultations
79 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More