Normal form (natural deduction)

In mathematical logic and proof theory, a derivation in normal form in the context of natural deduction refers to a proof which contains no detours — steps in which a formula is first introduced and then immediately eliminated.

The concept of normalization in natural deduction was introduced by Dag Prawitz in the 1960s as part of a general effort to analyze the structure of proofs and eliminate unnecessary reasoning steps. The associated normalization theorem establishes that every derivation in natural deduction can be transformed into normal form.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.