論理プログラミング 導出の効率化 論理プログラム ホーン節 ホーン集合に対する導出戦略 論理式の手続き的解釈 Prolog カット・オペレータ 閉世界仮説に基づく否定表現
節の新しい表記法 節： 負のリテラル 正のリテラル ホーン節
ホーン節（Horn clause） 確定節 ゴール節
ホーン節に対する導出戦略 SLD（Selective Linear Resolution for Definite Clause） （１）ゴール節を一方の親節とする． （２）ゴール節の最左端のリテラルに着目した導出を行う． （３）得られたゴール節を次の導出の一方の親節とする．
SLDは後向き推論である 後向き推論 ホーン節集合： 肯定式 肯定式
論理式の手続き的解釈 を証明するには を証明すればよい ホーン節は証明の手続きを表していると解釈できる を実行するには， を実行すればよい
論理プログラム Prolog 頭部（head） プログラム（確定節） 本体（body） 質問（ゴール節） インタプリタ（SLD導出）
Prologの基本動作 実行の成功 評価（SLD導出）の順序 （１） 成功 （２） （３） を直接評価した結果が真
例 節の選択は上から下へ 評価は左から右へ
バックトラックの例 スタック 失敗
実行の失敗とは b d b a 単一化可能な頭部をもつ節がない． 単一化可能な頭部をもつ節のすべてが本体の実行に失敗した． 述語の評価が偽である． バックトラックで再評価したとき別の選択肢がない． b a
バックトラックの制御 カット・オペレータ（！） 引数を持たない述語 実行時バックトラック用の選択肢情報を棄却 スタック
バックトラックの制御 カット・オペレータ（！） 引数を持たない述語 実行時バックトラック用の選択肢情報を棄却 スタック 成功
バックトラックの制御 カット・オペレータ（！） 引数を持たない述語 実行時バックトラック用の選択肢情報を棄却 スタック
バックトラックの制御 カット・オペレータ（！） 引数を持たない述語 実行時バックトラック用の選択肢情報を棄却 スタック 失敗
バックトラックの制御 カット・オペレータ（！） 引数を持たない述語 実行時バックトラック用の選択肢情報を棄却 失敗 スタック
カット・オペレータを用いた制御構造 条件分岐 繰り返し
例 好きなものは赤いりんごかみかんである． YES YES りんご？ 赤い？ NO NO YES 好きである みかん？ NO 好きでない
失敗による否定 否定の導入 成功 は失敗 である の実行 失敗 は成功 でない
閉世界仮説 失敗による否定は閉世界仮説に基づく 真なる事柄は すべて表示されている 失敗 閉世界仮説
失敗による否定 論理的否定 誤解 質問： 「P(x) の実行に失敗する」？ 「P である x は存在しない」？ ゴール節：
例 ？ 太郎が嫌いなものは何か？ 失敗 好きなものがある 太郎は嫌いなものはない（すべて好き） 失敗 誤解を招かない質問 太郎は桃が嫌い（閉世界仮説より） 失敗 誤解を招かない質問