自然演繹とは？
しぜんえんえき
仮定の導入と消去を基本とする、自然な推論スタイルを形式化した証明体系です。
自然演繹（natural deduction）とは、ゲルハルト・ゲンツェンが1934年に導入した証明体系で、各論理結合子に対して「導入則」と「消去則」を設けることで、人間の直観的な推論スタイルを形式化する。仮定の仮定・導入・消去という操作を基本とし、シーケント計算と並んで現代証明論の基礎をなす。カリー・ハワード対応により、自然演繹の証明と型付きλ計算のプログラムが対応することが知られる。
使い方・例文
∧の導入則は「P が証明でき Q も証明できるなら P∧Q が証明できる」と定式化され、自然演繹の基本規則の一例となる。
この用語をシェア
最終更新: