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.

[1] This logic-related article is a stub.

You can help Wikipedia by expanding it.