論理と推論 命題論理 推論 命題論理体系の健全性と完全性 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論規則 構文と意味 → 同値関係と標準形(節形式) 決定問題と意味木 推論 推論規則 推論の妥当性:論理的帰結 形式的証明 命題論理体系の健全性と完全性
論理による問題解決 論理式による知識の表現 証明(推論)による解決 知識 (論理式の集合) 推論規則 結論(答)
論理による問題解決 太郎は花子の父である. 次郎は太郎の父である. 父の父は祖父である. 推論規則
命題論理:構文 論理式 原子式,論理記号 整式(well-formed formula wff) (1) 原子式は整式である. 論理式 原子式,論理記号 整式(well-formed formula wff) (1) 原子式は整式である. (2) は整式である ⇒ は整式である. (3) , は整式である ⇒ は整式である. (4) 以上(1),(2),(3) より整式とわかるものだけが整式である. 論理記号 否定(negation) 連言(conjunction) 選言(disjunction) 含意(implication)
命題論理:意味 解釈: 原子式への真(T),偽(F)の割り当て 原子式 と解釈 : 論理記号の意味(真理表) T F
論理式の解釈 p q r T F p q r T F
同値関係 二重否定の法則(law of double negation): べき等律(idempotent law): 相補律(complementary law): 交換律(commutative law): 結合律(associative law): 分配律(distributive law): ド・モルガンの法則(De Morgan’s law): (矛盾律) (排中律)
標準形 節形式(clausal form) (連言標準形(conjunctive normal form CNF)) リテラル(literal): 原子式またはその否定形 節(clause): リテラルの選言 節形式: 節の連言 リテラル 節
節形式への変換 (1)含意記号を除去する. (2)否定記号を原子式の直前に移動する. (3)分配律を適用する.
恒真式と恒偽式 論理式全体 恒真式 恒偽式 充足可能 充足不能
決定問題 決定問題(decision problem) 意味木(semantic tree) 所与の論理式が恒真か否かを決定する問題 → 命題論理式の場合,有限時間で決定可能 意味木(semantic tree)
意味木 p q T F
推論 推論(inference, reasoning) 前提(premise)から結論(conclusion)を導くこと 前提① 前提② 前提① 鳥は卵を産む. 前提② 鶏は鳥である. 結論 鶏は卵を産む. 前提① 鳥は卵を産む. 前提② 猫は鳥である. 結論 猫は卵を産む. 前提① 前提② 結論 健全(sound)な推論 妥当(valid)な推論
推論の形式(推論規則) 肯定式(modus ponendo ponens) 否定式(modus tollend tollens) 三段論法(syllogism) (前提) (結論) (前提) (結論) (前提) (結論)
推論の妥当性 論理的帰結(logical consequence) 前提 が真となる任意の解釈において 結論 も真となる. (前提) 前提 が真となる任意の解釈において 結論 も真となる. (前提) (結論)
論理的帰結 :恒真 :恒偽 :充足不能
推論規則と恒真式 推論規則 恒真式 前件肯定規則 前提 結論 前件肯定式 対偶法 対偶律 選言除去規則(Dilemma規則) 選言除去式 選言三段論法 選言三段論法式 仮言三段論法 推移律
形式的証明 演繹体系 恒真式の集合 公理系 定理 推論規則 恒真式 妥当な推論
証明可能 形式的証明 公理系+推論規則 → 仮説からの演繹 公理+仮説 +推論規則 → 演繹定理
命題論理体系の性質 公理系の無矛盾性(consistency) いかなる論理式 についても と が 健全性(soundness) いかなる論理式 についても と が ともに証明可能となることはない. 健全性(soundness) 完全性(completeness)