構造証明論
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/12/16 07:47 UTC 版)
構造証明論は証明論の一分野であり、解析的証明の記述が可能な証明計算を研究する分野である。解析的証明の記法はゲンツェンがシークエント計算で導入したもので、そこではカット除去定理で表されていた。自然演繹の記法でも解析的証明は記述可能であることが Dag Prawitz によって示されている。その定義は若干複雑である。解析的証明は正規形であり、それは項書き換えにおける正規形と関連している。Jean-Yves Girard の proof net のような特殊な証明計算でも解析的証明の記法はサポートされている。 構造証明論は、カリー＝ハワード同型対応によって型理論とも関連している。カリー＝ハワード同型対応は、自然演繹計算における正規化のプロセスと型付きラムダ計算におけるベータ簡約の構造的類似性を示したものである。これはペール・マルティン＝レーフの直観主義的型理論の基盤となっており、カルテシアン閉圏も含めた三者の同型対応に拡張されることが多い。 言語学では、自然言語の形式意味論に構造証明論を用いて定式化したものとして、Type Logical Grammar、範疇文法、モンタギュー文法がある。
※この「構造証明論」の解説は、「証明論」の解説の一部です。
「構造証明論」を含む「証明論」の記事については、「証明論」の概要を参照ください。
ウィキペディア小見出し辞書の「構造証明論」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。
お問い合わせ。
- 構造証明論のページへのリンク
