充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性.

Presentation on theme: "充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性."— Presentation transcript:

1 充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性

2 一階述語論理式の充足不能性 任意の閉式 　　　　　 （全称記号のみで限量された閉式） 標準的な解釈 スコーレム標準形 エルブラン解釈

3 標準形 スコーレム標準形（Skolem normal form) ：全称束縛冠頭形 ：節形式 ：節

4 スコーレム標準形への変換 （１） のみからなる論理式にして を原子式の直前に移動する． （２）束縛変数の標準化をする．
（１）　　　　　 のみからなる論理式にして　　を原子式の直前に移動する． （２）束縛変数の標準化をする． （３）スコーレム関数を導入して　　を除去する． （４）冠頭形に変換する． （５）母式を節形式に変換する．

5 スコーレム関数の導入

6 変換に役立つ同値関係 （１）変数名の付け替え （２） （３）論理式　　が変数　　を含まないとき （４）

7 例 同値な変換ではない！

8 節集合 閉式： スコーレム標準形： 節集合： 　　：充足不能　　　　　：充足不能

9 エルブラン領域 エルブラン領域 エルブラン基底 基礎節 節集合 S に現れる個体定数,関数記号を用いて作られる項（基礎項）全体の集合

10 例 基礎節の集合：

11 エルブラン解釈 エルブラン解釈 個体定数 a： 関数記号 f： 述語記号： 基礎例に真偽を割当てる． HB(S)の部分集合に対応
述語記号：　 基礎例に真偽を割当てる． HB(S)の部分集合に対応 一つのエルブラン解釈

12 エルブラン解釈の充足可能性 節集合 S が充足可能ならば，S を充足するエルブラン解釈が存在する． ある解釈 が S を充足するとき，
基礎例　　　　　　 の真理値を とすれば，このエルブラン解釈は S を充足する．

13 例

14 エルブランの定理 節集合 S が充足不能ならば， そのときに限り S を充足するエルブラン解釈は存在しない．
基礎例にT,Fを割当 充足可能なエルブラン解釈が存在しなければ，その節集合は充足不能である． ある基礎節がFになるとこのエルブラン解釈は節集合を充足できない 充足不能な基礎節の集合

15 エルブランの定理 節集合 S が充足不能ならば， そのときに限り S を充足するエルブラン解釈は存在しない． エルブランの定理
　　有限部分集合で充足不能な集合が存在する．

16 導出（resolution） 基礎節　 がリテラル　を含み，基礎節　　がその相補的リテラル　　 を含むとき，　　から　を除去した節と　　 から　　 を除去した節の選言をとってできる節を　　と　　の導出節（resolvent）といい，この操作を導出という． 導出は妥当な推論である.

17 導出原理 節集合　 の充足不能性の証明

18 導出原理の完全性と健全性 完全性 　　節集合Sが充足不能　⇒　空節□ S の意味木 の意味木

19 導出原理の完全性と健全性 健全性 空節□ ⇒ 節集合Sは充足不能 節集合S （充足可能と仮定） 導出 （妥当な推論） {導出節}
（充足可能） 矛盾 （充足不能） 空節□を含む節集合

20 例 ？ ：充足不能？ ：節集合

21 例