Normal form (natural deduction)

An inference of natural deduction is a normal form, according to Dag Prawitz, if no formula occurrence is both the principal premise of an elimination rule and the conclusion of an introduction rule.

This article is issued from Wikipedia - version of the 1/10/2013. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.