推論規則
| 演繹の推論規則 |
|---|
| 命題計算 |
|
モーダスポネンス |
| 述語計算 |
| 存在例化 |
 カテゴリ:推論規則 |
推論規則（すいろんきそく、英: rule of inference, inference rule, transformation rule）とは、論理式から他の論理式を導く推論の規則である。
記号、公理、代入規則、推論規則によって理論を形式化したものを公理系という。 公理は記号だけで記述されるが、推論規則や代入規則はこれらの記号について述べているメタ言語で記述される。 恒真式 （トートロジー）から推論規則を導くと妥当性のある推論になる。
古典論理における推論規則
古典論理における代表的な推論規則を以下に示す。（⊢は推論を表すメタ言語の記号であり、A0, …, An-1 ⊢ BはA0, …, An-1からBが導かれることを示す。）
演繹
- 前件肯定 P, P→Q ⊢ Q
- 後件否定 ￢Q, P→Q ⊢ ￢P
- 否定導入 P → ⊥ ⊢ ￢P
- 普遍例化 ∀xψ(x) ⊢ ψ(a)
- 存在汎化 ψ(a) ⊢ ∃xψ(x)
- 二重否定の除去 ￢￢P ⊢ P
- 二重否定の導入 P ⊢ ￢￢P
- 選言三段論法 P∨Q, ￢P ⊢ Q
- 仮言三段論法 P→Q, Q→R ⊢ P→R
- 導出 l∨P, ￢l∨Q ⊢ P∨Q
アブダクション（仮説形成）
- 後件肯定 Q, P→Q ⊢ P