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

m
(内容の大幅増強)
# <math>P_1, \dots ,P_n</math> を[[スコーレム標準形|スコーレム連言標準形]] <math>C_1, \dots ,C_n</math> に変換する。
# <math>\lnot P</math> を[[スコーレム標準形|スコーレム連言標準形]] <math>C</math> に変換する。
# もし <math>C, C_1, \dots ,C_n</math> の反駁が存在すれば、 <math>FP</math> は <math>P_1, \dots ,P_n</math> の論理的帰結である。
::あるいは、別の表現をすれば、
::* <math>C, C_1, \dots ,C_n</math> が充足不能