Herbrand-Confluence
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 whic...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2013-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/727/pdf |
| _version_ | 1797268690594430976 |
|---|---|
| author | Stefan Hetzl Lutz Straßburger |
| author_facet | Stefan Hetzl Lutz Straßburger |
| author_sort | Stefan Hetzl |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:29Z |
| format | Article |
| id | doaj.art-4d39ecc186364a339c0563779d3af15b |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:29Z |
| publishDate | 2013-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-4d39ecc186364a339c0563779d3af15b2024-03-08T09:30:37ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742013-12-01Volume 9, Issue 410.2168/LMCS-9(4:24)2013727Herbrand-ConfluenceStefan Hetzlhttps://orcid.org/0000-0002-6461-5982Lutz StraßburgerWe 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.https://lmcs.episciences.org/727/pdfcomputer science - logic in computer science |
| spellingShingle | Stefan Hetzl Lutz Straßburger Herbrand-Confluence Logical Methods in Computer Science computer science - logic in computer science |
| title | Herbrand-Confluence |
| title_full | Herbrand-Confluence |
| title_fullStr | Herbrand-Confluence |
| title_full_unstemmed | Herbrand-Confluence |
| title_short | Herbrand-Confluence |
| title_sort | herbrand confluence |
| topic | computer science - logic in computer science |
| url | https://lmcs.episciences.org/727/pdf |
| work_keys_str_mv | AT stefanhetzl herbrandconfluence AT lutzstraßburger herbrandconfluence |