Which proofs can be computed by cut elimination

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 ?