推論規則

出典: フリー百科事典『ウィキペディア（Wikipedia）』

推論規則（すいろんきそく）とは、論理式から他の論理式を導く規則である。

公理、代入規則、推論規則によって理論を形式化したものは公理系である。 公理は対象語の記号だけで記述されるが、推論規則や代入規則はこれらの記号について述べているメタ言語で記述される。 推論規則はトートロジーから導くのが妥当である。

代表的な推論規則を以下に示す。（‘￢’は否定、‘→’は内含、他は論理式）

• 前件肯定　［Ｐ，Ｐ→Ｑ］→Ｑ
• 後件否定　［￢Ｑ，Ｐ→Ｑ］→￢Ｐ
• 普遍例化　∀ｘＦ（ｘ）→Ｆ（ｙ）
• 存在一般化　Ｆ（ｙ）→∃ｘＦ（ｘ）
• その他

[編集] 関連項目

• シークエント計算