Stefan Hetzl ; Lutz Straßburger - Herbrand-Confluence

lmcs:727 - Logical Methods in Computer Science, December 18, 2013, Volume 9, Issue 4 - https://doi.org/10.2168/LMCS-9(4:24)2013
Herbrand-Confluence

Authors: Stefan Hetzl ORCID-iD; Lutz Straßburger

    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.


    Volume: Volume 9, Issue 4
    Published on: December 18, 2013
    Accepted on: June 25, 2015
    Submitted on: January 29, 2013
    Keywords: Computer Science - Logic in Computer Science
    Fundings :
      Source : OpenAIRE Research Graph
    • Algorithmic Structuring and Compression of Proofs; Funder: Austrian Science Fund (FWF); Code: P 25160

    Linked data

    Source : ScholeXplorer HasVersion DOI 10.48550/arxiv.1310.8156
    • 10.48550/arxiv.1310.8156
    Herbrand-Confluence
    Hetzl, Stefan ; Stra��burger, Lutz ;

    2 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 388 times.
    This article's PDF has been downloaded 205 times.