充足不能性と導出原理 充足不能性の証明 スコーレム標準形 エルブラン解釈 導出原理 基礎節に対する導出 導出原理の完全性と健全性
一階述語論理式の充足不能性 任意の閉式 （全称記号のみで限量された閉式） 標準的な解釈 スコーレム標準形 エルブラン解釈
標準形 スコーレム標準形（Skolem normal form) ：全称束縛冠頭形 ：節形式 ：節
スコーレム標準形への変換 （１） のみからなる論理式にして を原子式の直前に移動する． （２）束縛変数の標準化をする． （１） のみからなる論理式にして を原子式の直前に移動する． （２）束縛変数の標準化をする． （３）スコーレム関数を導入して を除去する． （４）冠頭形に変換する． （５）母式を節形式に変換する．
スコーレム関数の導入
変換に役立つ同値関係 （１）変数名の付け替え （２） （３）論理式 が変数 を含まないとき （４）
例 同値な変換ではない！
節集合 閉式： スコーレム標準形： 節集合： ：充足不能 ：充足不能
エルブラン領域 エルブラン領域 エルブラン基底 基礎節 節集合 S に現れる個体定数,関数記号を用いて作られる項（基礎項）全体の集合
例 基礎節の集合：
エルブラン解釈 エルブラン解釈 個体定数 a： 関数記号 f： 述語記号： 基礎例に真偽を割当てる． HB(S)の部分集合に対応 述語記号： 基礎例に真偽を割当てる． HB(S)の部分集合に対応 一つのエルブラン解釈
エルブラン解釈の充足可能性 節集合 S が充足可能ならば，S を充足するエルブラン解釈が存在する． ある解釈 が S を充足するとき， 基礎例 の真理値を とすれば，このエルブラン解釈は S を充足する．
例
エルブランの定理 節集合 S が充足不能ならば， そのときに限り S を充足するエルブラン解釈は存在しない． 基礎例にT,Fを割当 充足可能なエルブラン解釈が存在しなければ，その節集合は充足不能である． ある基礎節がFになるとこのエルブラン解釈は節集合を充足できない 充足不能な基礎節の集合
エルブランの定理 節集合 S が充足不能ならば， そのときに限り S を充足するエルブラン解釈は存在しない． エルブランの定理 有限部分集合で充足不能な集合が存在する．
導出（resolution） 基礎節 がリテラル を含み，基礎節 がその相補的リテラル を含むとき， から を除去した節と から を除去した節の選言をとってできる節を と の導出節（resolvent）といい，この操作を導出という． 導出は妥当な推論である.
導出原理 節集合 の充足不能性の証明
導出原理の完全性と健全性 完全性 節集合Sが充足不能 ⇒ 空節□ S の意味木 の意味木
導出原理の完全性と健全性 健全性 空節□ ⇒ 節集合Sは充足不能 節集合S （充足可能と仮定） 導出 （妥当な推論） {導出節} （充足可能） 矛盾 （充足不能） 空節□を含む節集合
例 ？ ：充足不能？ ：節集合
例