Which proofs can be computed by cut elimination
22
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe et accède à tout notre catalogue !
Découvre YouScribe et accède à tout notre catalogue !
22
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
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
Langue
English
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
