「導出原理」の版間の差分

(誤)a_i → (正)a_j
m
((誤)a_i → (正)a_j)
'''導出'''(どうしゅつ)とは、[[数理論理学]]における一つの[[演繹]]方法である。[[定理自動証明]]において一般的に使われる手法。
 
導出おいて二つの[[節]]より新しい節を導きだす演繹ルールを導出原理といい、一方の節に含まれる命題と、他方の節に含まれるその命題の否定をのぞき、その他の命題の[[論理和]]をとることで、新しい節を得ることをいう。式で表せば、命題<math>a_i</math>が命題<math>b_ib_j</math>の否定である時、
 
<math>\frac{
匿名利用者