推論規則(すいろんきそく、英: 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)