Which proofs can be computed by cut elimination

Stefan Hetzl

Description

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 ?

Sujets

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

Informations

• Publié par: chaeh
• Nombre de lectures: 12
• Langue: English

Extrait

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