Iowa Type Theory Commute

Normalization in natural deduction


Listen Later

This episode explains the idea of normalization of proofs in natural deduction.  We want to eliminate so-called detours in proofs, which occur when an introduction is immediately followed by an elimination.

...more
View all episodesView all episodes
Download on the App Store

Iowa Type Theory CommuteBy Aaron Stump

  • 5
  • 5
  • 5
  • 5
  • 5

5

16 ratings