Which proofs can be computed by cut elimination

Which proofs can be computed by cut elimination

22

pages

English

Documents

Écrit par
Stefan Hetzl

Publié par
chaeh

Lire un extrait

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Découvre YouScribe en t'inscrivant gratuitement

22

pages

English

Ebook

Lire un extrait

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

Nombre de lectures

12

Langue

English

Niveau: Supérieur
Which proofs can be computed by cut-elimination? Stefan Hetzl Institute of Discrete Mathematics and Geometry Vienna University of Technology ASL 2012 North American Annual Meeting Special Session: Structural Proof Theory and Computing Madison, Wisconsin April 3, 2012 1/ 17

called confluent

reduction strategy

local reduction

curry-howard correspondence

cut elimination

proof rewriting

pi ?

Publié par

Nombre de lectures

12

Langue

English

University of Vienna Reduction strategy Curry?Howard correspondence Cut-elimination theorem

Which proofs can be computed by
cut-elimination?

Stefan Hetzl
Institute of Discrete Mathematics and Geometry
Vienna University of Technology

ASL 2012 North American Annual Meeting
Special Session:Structural Proof Theory and Computing

Madison, Wisconsin

April 3, 2012

1/ 17

Gentzen’s proof

G. Gentzen:Untersuchungen ¨ber das logische Schließen I,
Mathematische Zeitschrift, 39(2), 176–210, 1934

=⇒Cut-elimination by local proof rewriting steps

2/ 17

Univers
Ebooks
Livres audio
Presse
Podcasts
BD
Documents

© 2010-2024 YouScribe

Livre audio en ligne - Développement personnel Livre en ligne Tout le catalogue Tous les Intérêts