The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
From MaRDI portal
Publication:5204803
DOI10.1098/rsta.2018.0038zbMath1436.03293OpenAlexW2913653100WikidataQ92982889 ScholiaQ92982889MaRDI QIDQ5204803
Publication date: 5 December 2019
Published in: Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1098/rsta.2018.0038
Specification and verification (program logics, model checking, etc.) (68Q60) Proof theory in general (including proof-theoretic semantics) (03F03)
Related Items (1)
Uses Software
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
- Linear logic, coherence and dinaturality
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Extension without cut
- Categorical proof theory of classical propositional calculus
- CERES: An analysis of Fürstenberg's proof of the infinity of primes
- Don't eliminate cut
- Handsome proof-nets: Perfect matchings and cographs
- Theorem proving modulo
- Isabelle/HOL. A proof assistant for higher-order logic
- From syntactic proofs to combinatorial proofs
- Untersuchungen über das logische Schliessen. I
- Polarized proof-nets and \(\lambda \mu\)-calculus
- Proofs without syntax
- Order-enriched categorical models of the classical sequent calculus
- Control categories and duality: on the categorical semantics of the lambda-mu calculus
- The duality of computation
- On the proof complexity of deep inference
- On the Power of Substitution in the Calculus of Structures
- Rewriting with Linear Inferences in Propositional Logic
- A Local System for Classical Logic
- A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
- A Proposal for Broad Spectrum Proof Certificates
- Propositional proof systems, the consistency of first order theories and the complexity of computations
- The Beginning of Model Checking: A Personal Perspective
- Normalisation Control in Deep Inference via Atomic Flows
- The Four Colour Theorem: Engineering of a Formal Proof
- Proof Complexity of the Cut-free Calculus of Structures
- On the Word Problem for ${\it \Sigma\Pi}$ -Categories, and the Properties of Two-Way Communication
- Refutations by Matings
- The relative efficiency of propositional proof systems
- Classical logic, continuation semantics and abstract machines
- Hilbert's Twenty-Fourth Problem
- No proof nets for MLL with units
- Identity of Proofs Based on Normalization and Generality
- Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
- Abella: A System for Reasoning about Relational Specifications
- From Proof Nets to the Free *-Autonomous Category
- Computer Science Logic
- A Machine-Checked Proof of the Odd Order Theorem
- A Characterization of Medial as Rewriting Rule
- Deductive systems and categories
- Typed Lambda Calculi and Applications
- Proof nets and semi-star-autonomous categories
- Proof theory in the abstract
This page was built for publication: The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
