some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

SPECIAL ISSUES

   Recent

   In Progress

   Archive

   Proposal

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

SPECIAL ISSUE:
Special Issue for the Conference on Computer Science Logic (CSL) 2012



Herbrand-Confluence

©Stefan Hetzl, INRIA Saclay -- Ile-de-France
©Lutz Straßburger, 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.

Publication date: December 18, 2013

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-9(4:24)2013

Hit Counts: 5246

Creative Commons