シークエント計算
カット規則
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2018/12/29 05:00 UTC 版)
「カット規則」とは、シークエント計算の一般的な推論規則であり、次のような形式で表現される。 (1) ( A , B , … ) ⊢ C {\displaystyle (A,B,\ldots )\vdash C} と (2) C ⊢ ( D , E , … ) {\displaystyle C\vdash (D,E,\ldots )} とが、ともに成立しているとき、次を導出できる。 (3) ( A , B , … ) ⊢ ( D , E , … ) {\displaystyle (A,B,\ldots )\vdash (D,E,\ldots )} すなわち、ここでは論理式 C が帰結からカットされている。
※この「カット規則」の解説は、「カット除去定理」の解説の一部です。
「カット規則」を含む「カット除去定理」の記事については、「カット除去定理」の概要を参照ください。
ウィキペディア小見出し辞書の「カット規則」の項目はプログラムで機械的に意味や本文を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ。
- カット規則のページへのリンク
