Towards Hilbert's 24th Problem: Combinatorial Proof Invariants

DOI10.1016/j.entcs.2006.05.036zbMath1262.03120OpenAlexW2082734160MaRDI QIDQ4917988

Dominic J. D. Hughes

Publication date: 3 May 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2006.05.036

zbMATH Keywords

sequent calculusHerbrand's theoremcombinatorial proofHilbert's 24th problem

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Structure of proofs (03F07)

Related Items (7)

Combinatorial flows as bicolored atomic flows ⋮ A semiclassical heat kernel proof of the Poincaré-Hopf theorem ⋮ Proof nets for classical logic ⋮ A new mapping between combinatorial proofs and sequent calculus proofs read out from logical flow graphs ⋮ The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem ⋮ Discussing Hilbert's 24th problem ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Categorical proof theory of classical propositional calculus
• A decidable fragment of predicate calculus
• Complement reducible graphs
• A game semantics for linear logic
• The structure of multiplicatives
• New foundations for the geometry of interaction
• Handsome proof-nets: Perfect matchings and cographs
• Coherence completions of categories
• Modular elliptic curves and Fermat's Last Theorem
• Ring-theoretic properties of certain Hecke algebras
• An approach to a systematic theorem proving procedure in first-order logic
• Proofs without syntax
• A generalization of the functorial calculus
• Coherence in closed categories
• Synthesis of the resolution method with the inverse method
• Order-enriched categorical models of the classical sequent calculus
• Theorem Proving via General Matings
• A new constructive logic: classic logic
• The relative efficiency of propositional proof systems
• Graph Classes: A Survey
• Games and full completeness for multiplicative linear logic
• A new deconstructive logic: linear logic
• Hilbert's Twenty-Fourth Problem
• Proof Nets for Classical Logic
• The Complexity of Propositional Proofs
• Traced monoidal categories
• Proof nets for unit-free multiplicative-additive linear logic
• From Proof Nets to the Free *-Autonomous Category
• Computer Science Logic
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic
• Typed Lambda Calculi and Applications
• Proof theory in the abstract

This page was built for publication: Towards Hilbert's 24th Problem: Combinatorial Proof Invariants