Combinatorial Proofs and Decomposition Theorems for First-order Logic
| Autor: | Jui-Hsuan Wu, Dominic J. D. Hughes, Lutz Straßburger |
|---|---|
| Přispěvatelé: | Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion (PARTOUT), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), logic group, University of California [Berkeley] (UC Berkeley), University of California (UC)-University of California (UC), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, University of California [Berkeley], University of California-University of California |
| Jazyk: | angličtina |
| Rok vydání: | 2021 |
| Předmět: |
Soundness
FOS: Computer and information sciences Computer Science - Logic in Computer Science Computer science 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Combinatorial proof Computer Science::Computation and Language (Computational Linguistics and Natural Language and Speech Processing) 0102 computer and information sciences 16. Peace & justice Mathematical proof 01 natural sciences First-order logic Logic in Computer Science (cs.LO) Algebra TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Completeness (logic) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Gödel's completeness theorem 0101 mathematics Rule of inference Deep inference |
| Zdroj: | LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-13, ⟨10.1109/LICS52264.2021.9470579⟩ |
| DOI: | 10.1109/LICS52264.2021.9470579⟩ |
| Popis: | We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof system based on inference rules, a combinatorial proof is a syntax-free presentation of a proof that is independent from any set of inference rules. We show that the two proof representations are related via a deep inference decomposition theorem that establishes a new kind of normal form for syntactic proofs. This yields (a) a simple proof of soundness and completeness for first-order combinatorial proofs, and (b) a full completeness theorem: every combinatorial proof is the image of a syntactic proof. To be published in LICS 2021. This is the author version of the paper with full proofs in the appendix |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|