The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem (Q5204803): Difference between revisions

Latest revision as of 16:19, 30 December 2024

scientific article; zbMATH DE number 7140441

Language	Label	Description	Also known as
English	The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem	scientific article; zbMATH DE number 7140441

Statements

instance of

scholarly article

0 references

title

The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem (English)

0 references

author

Lutz Straßburger

0 references

published in

Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences

0 references

publication date

5 December 2019

0 references

zbMATH Keywords

proof theory

0 references

Hilbert's 24th problem

0 references

identity of proofs

0 references

combinatorial proofs

0 references

describes a project that uses

0 references

0 references

0 references

0 references

0 references

0 references

MaRDI publication profile

0 references

full work available at URL

https://doi.org/10.1098/rsta.2018.0038

0 references

cites work

Hilbert's Twenty-Fourth Problem

0 references

The Four Colour Theorem: Engineering of a Formal Proof

0 references

A Machine-Checked Proof of the Odd Order Theorem

0 references

Abella: A System for Reasoning about Relational Specifications

0 references

Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.

0 references

A Proposal for Broad Spectrum Proof Certificates

0 references

Identity of Proofs Based on Normalization and Generality

0 references

Q5559220

0 references

CERES: An analysis of Fürstenberg's proof of the infinity of primes

0 references

Deductive systems and categories

0 references

Q5595187

0 references

Q3727946

0 references

Q3827993

0 references

Linear logic, coherence and dinaturality

0 references

From Proof Nets to the Free *-Autonomous Category

0 references

Proof nets and semi-star-autonomous categories

0 references

Q4255509

0 references

Categorical proof theory of classical propositional calculus

0 references

Proof theory in the abstract

0 references

Q3376920

0 references

Q5423982

0 references

Untersuchungen über das logische Schliessen. I

0 references

Don't eliminate cut

0 references

The relative efficiency of propositional proof systems

0 references

Propositional proof systems, the consistency of first order theories and the complexity of computations

0 references

On the proof complexity of deep inference

0 references

Extension without cut

0 references

On the Power of Substitution in the Calculus of Structures

0 references

Proof Complexity of the Cut-free Calculus of Structures

0 references

A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae

0 references

Isabelle/HOL. A proof assistant for higher-order logic

0 references

Theorem proving modulo

0 references

Q4499084

0 references

No proof nets for MLL with units

0 references

Q5560258

0 references

Q2753601

0 references

The duality of computation

0 references

Classical logic, continuation semantics and abstract machines

0 references

Control categories and duality: on the categorical semantics of the lambda-mu calculus

0 references

Polarized proof-nets and $\lambda \mu$-calculus

0 references

Order-enriched categorical models of the classical sequent calculus

0 references

Q5423981

0 references

On the Word Problem for ${\it \Sigma\Pi}$ -Categories, and the Properties of Two-Way Communication

0 references

Computer Science Logic

0 references

Refutations by Matings

0 references

Typed Lambda Calculi and Applications

0 references

Linear logic

0 references

Normalisation Control in Deep Inference via Atomic Flows

0 references

Rewriting with Linear Inferences in Propositional Logic

0 references

Proofs without syntax

0 references

Q5111329

0 references

Handsome proof-nets: Perfect matchings and cographs

0 references

Towards Hilbert's 24th Problem: Combinatorial Proof Invariants

0 references

A Characterization of Medial as Rewriting Rule

0 references

From syntactic proofs to combinatorial proofs

0 references

Q4783301

0 references

A Local System for Classical Logic

0 references

The Beginning of Model Checking: A Personal Perspective

0 references

Identifiers

zbMATH Open document ID

1436.03293

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

0 references

10.1098/RSTA.2018.0038

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:5204803

@@ Property / DOI @@
-.1098/rsta.2018.0038
@@ Property / DOI: 10.1098/rsta.2018.0038 / rank @@
-Normal rank
@@ Property / describes a project that uses @@
+Abella
@@ Property / describes a project that uses: Abella / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CERES
@@ Property / describes a project that uses: CERES / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+seL4
@@ Property / describes a project that uses: seL4 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1098/rsta.2018.0038
+Normal rank
@@ Property / OpenAlex ID @@
+W2913653100
@@ Property / OpenAlex ID: W2913653100 / rank @@
+Normal rank
@@ Property / cites work @@
+Hilbert's Twenty-Fourth Problem
@@ Property / cites work: Hilbert's Twenty-Fourth Problem / rank @@
+Normal rank
@@ Property / cites work @@
+The Four Colour Theorem: Engineering of a Formal Proof
+Normal rank
@@ Property / cites work @@
+A Machine-Checked Proof of the Odd Order Theorem
@@ Property / cites work: A Machine-Checked Proof of the Odd Order Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Abella: A System for Reasoning about Relational Specifications
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+A Proposal for Broad Spectrum Proof Certificates
@@ Property / cites work: A Proposal for Broad Spectrum Proof Certificates / rank @@
+Normal rank
@@ Property / cites work @@
+Identity of Proofs Based on Normalization and Generality
+Normal rank
@@ Property / cites work @@
+Q5559220
@@ Property / cites work: Q5559220 / rank @@
+Normal rank
@@ Property / cites work @@
+CERES: An analysis of Fürstenberg's proof of the infinity of primes
+Normal rank
@@ Property / cites work @@
+Deductive systems and categories
@@ Property / cites work: Deductive systems and categories / rank @@
+Normal rank
@@ Property / cites work @@
+Q5595187
@@ Property / cites work: Q5595187 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3727946
@@ Property / cites work: Q3727946 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3827993
@@ Property / cites work: Q3827993 / rank @@
+Normal rank
@@ Property / cites work @@
+Linear logic, coherence and dinaturality
@@ Property / cites work: Linear logic, coherence and dinaturality / rank @@
+Normal rank
@@ Property / cites work @@
+From Proof Nets to the Free *-Autonomous Category
@@ Property / cites work: From Proof Nets to the Free *-Autonomous Category / rank @@
+Normal rank
@@ Property / cites work @@
+Proof nets and semi-star-autonomous categories
@@ Property / cites work: Proof nets and semi-star-autonomous categories / rank @@
+Normal rank
@@ Property / cites work @@
+Q4255509
@@ Property / cites work: Q4255509 / rank @@
+Normal rank
@@ Property / cites work @@
+Categorical proof theory of classical propositional calculus
+Normal rank
@@ Property / cites work @@
+Proof theory in the abstract
@@ Property / cites work: Proof theory in the abstract / rank @@
+Normal rank
@@ Property / cites work @@
+Q3376920
@@ Property / cites work: Q3376920 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5423982
@@ Property / cites work: Q5423982 / rank @@
+Normal rank
@@ Property / cites work @@
+Untersuchungen über das logische Schliessen. I
@@ Property / cites work: Untersuchungen über das logische Schliessen. I / rank @@
+Normal rank
@@ Property / cites work @@
+Don't eliminate cut
@@ Property / cites work: Don't eliminate cut / rank @@
+Normal rank
@@ Property / cites work @@
+The relative efficiency of propositional proof systems
+Normal rank
@@ Property / cites work @@
+Propositional proof systems, the consistency of first order theories and the complexity of computations
+Normal rank
@@ Property / cites work @@
+On the proof complexity of deep inference
@@ Property / cites work: On the proof complexity of deep inference / rank @@
+Normal rank
@@ Property / cites work @@
+Extension without cut
@@ Property / cites work: Extension without cut / rank @@
+Normal rank
@@ Property / cites work @@
+On the Power of Substitution in the Calculus of Structures
+Normal rank
@@ Property / cites work @@
+Proof Complexity of the Cut-free Calculus of Structures
+Normal rank
@@ Property / cites work @@
+A Quasipolynomial Cut-Elimination Procedure in Deep Inference via Atomic Flows and Threshold Formulae
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Theorem proving modulo
@@ Property / cites work: Theorem proving modulo / rank @@
+Normal rank
@@ Property / cites work @@
+Q4499084
@@ Property / cites work: Q4499084 / rank @@
+Normal rank
@@ Property / cites work @@
+No proof nets for MLL with units
@@ Property / cites work: No proof nets for MLL with units / rank @@
+Normal rank
@@ Property / cites work @@
+Q5560258
@@ Property / cites work: Q5560258 / rank @@
+Normal rank
@@ Property / cites work @@
+Q2753601
@@ Property / cites work: Q2753601 / rank @@
+Normal rank
@@ Property / cites work @@
+The duality of computation
@@ Property / cites work: The duality of computation / rank @@
+Normal rank
@@ Property / cites work @@
+Classical logic, continuation semantics and abstract machines
+Normal rank
@@ Property / cites work @@
+Control categories and duality: on the categorical semantics of the lambda-mu calculus
+Normal rank
@@ Property / cites work @@
+Polarized proof-nets and \(\lambda \mu\)-calculus
@@ Property / cites work: Polarized proof-nets and \(\lambda \mu\)-calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Order-enriched categorical models of the classical sequent calculus
+Normal rank
@@ Property / cites work @@
+Q5423981
@@ Property / cites work: Q5423981 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Word Problem for ${\it \Sigma\Pi}$ -Categories, and the Properties of Two-Way Communication
+Normal rank
@@ Property / cites work @@
+Computer Science Logic
@@ Property / cites work: Computer Science Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Refutations by Matings
@@ Property / cites work: Refutations by Matings / rank @@
+Normal rank
@@ Property / cites work @@
+Typed Lambda Calculi and Applications
@@ Property / cites work: Typed Lambda Calculi and Applications / rank @@
+Normal rank
@@ Property / cites work @@
+Linear logic
@@ Property / cites work: Linear logic / rank @@
+Normal rank
@@ Property / cites work @@
+Normalisation Control in Deep Inference via Atomic Flows
+Normal rank
@@ Property / cites work @@
+Rewriting with Linear Inferences in Propositional Logic
+Normal rank
@@ Property / cites work @@
+Proofs without syntax
@@ Property / cites work: Proofs without syntax / rank @@
+Normal rank
@@ Property / cites work @@
+Q5111329
@@ Property / cites work: Q5111329 / rank @@
+Normal rank
@@ Property / cites work @@
+Handsome proof-nets: Perfect matchings and cographs
+Normal rank
@@ Property / cites work @@
+Towards Hilbert's 24th Problem: Combinatorial Proof Invariants
+Normal rank
@@ Property / cites work @@
+A Characterization of Medial as Rewriting Rule
@@ Property / cites work: A Characterization of Medial as Rewriting Rule / rank @@
+Normal rank
@@ Property / cites work @@
+From syntactic proofs to combinatorial proofs
@@ Property / cites work: From syntactic proofs to combinatorial proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4783301
@@ Property / cites work: Q4783301 / rank @@
+Normal rank
@@ Property / cites work @@
+A Local System for Classical Logic
@@ Property / cites work: A Local System for Classical Logic / rank @@
+Normal rank
@@ Property / cites work @@
+The Beginning of Model Checking: A Personal Perspective
+Normal rank
@@ Property / DOI @@
+.1098/RSTA.2018.0038
@@ Property / DOI: 10.1098/RSTA.2018.0038 / rank @@
+Normal rank