Which proofs can be computed by cut elimination

-

English
22 Pages
Read an excerpt
Gain access to the library to view online
Learn more

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 ?


Subjects

Informations

Published by
Reads 12
Language English
Report a problem

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