Skip to Main content Skip to Navigation
Conference papers

Combinatorial Proofs and Decomposition Theorems for First-order Logic

Lutz Straßburger 1 Dominic Hughes 2 Jui-Hsuan Wu 1
1 PARTOUT - Automatisation et ReprésenTation: fOndation du calcUl et de la déducTion
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : 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 firstorder combinatorial proofs, and (b) a full completeness theorem: every combinatorial proof is the image of a syntactic proof.
Document type :
Conference papers
Complete list of metadata
Contributor : Lutz Straßburger Connect in order to contact the contributor
Submitted on : Thursday, October 7, 2021 - 3:26:54 PM
Last modification on : Saturday, October 9, 2021 - 4:02:02 AM


Files produced by the author(s)



Lutz Straßburger, Dominic Hughes, Jui-Hsuan Wu. Combinatorial Proofs and Decomposition Theorems for First-order Logic. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-13, ⟨10.1109/LICS52264.2021.9470579⟩. ⟨hal-03369764⟩



Record views


Files downloads