ソフトウェア科学特論: Prologと命題論理

Table of Contents

1 概要

Prologの概要等については,以下のWebページを参照のこと.

1.1 注意

本Webページ(およびPDF)の作成には Emacs org-mode を用いており, 数式等の表示は MathJax を用いています. IEでは正しく表示されないことがあるため, Firefox, Safari等のWebブラウザでJavaScriptを有効にしてお使いください. また org-info.js を利用しており, 「m」キーをタイプするとinfoモードでの表示になります. 利用できるショートカットは「?」で表示されます.

2 インストール

以下の処理系のどちらかをインストールする.

なお,神戸大学情報基盤センターの教育用端末には, SWI-Prolog がインストールされている.

3 命題論理式

3.1 命題論理式

以下のプログラムを prop01.pl として保存する.

1:  formula(false).
2:  formula(true).
3:  formula(P) :- atom(P).
4:  formula(and(A,B)) :- formula(A), formula(B).
5:  formula(or(A,B)) :- formula(A), formula(B).
6:  formula(imp(A,B)) :- formula(A), formula(B).
7:  formula(neg(A)) :- formula(A).
  • 1, 2行目は,それぞれfalse, trueがformulaであることを表している.
  • 3行目は,任意の記号(atom)がformulaであることを表している.
  • 4行目は,Aがformulaであり,かつBがformulaであるならば, and(A,B)はformulaであることを表している.
  • 5行目以降は,同様に or(A,B), imp(A,B), neg(A) がformulaである条件を定義している.

3.1.1 実行例

$ /opt/local/bin/swipl
...
?- [prop01].
% prop01 compiled 0.00 sec, 2,104 bytes
true.

?- formula(and(p,imp(neg(q),true))).
yes

3.2 部分論理式

以下のPrologプログラムは部分論理式の関係を定義している (prop02.pl).

1:  subformula(A, A).
2:  subformula(A, and(B,C)) :- subformula(A, B) ; subformula(A, C).
3:  subformula(A, or(B,C)) :- subformula(A, B) ; subformula(A, C).
4:  subformula(A, imp(B,C)) :- subformula(A, B) ; subformula(A, C).
5:  subformula(A, neg(B)) :- subformula(A, B).
  • 1行目は,A自身がAのsubformulaであることを表している.
  • 2行目は,AがBのsubformulaであるか,またはCのsubformulaであれば, Aはand(B,C)のsubformulaであることを表している.
  • 3行目以降も同様にAがor(B,C), imp(B,C), neg(B)の subformulaである条件を定義している.

3.2.1 実行例

?- subformula(A, and(p,imp(neg(q),true))).
A = and(p,imp(neg(q),true)) ? ;
A = p ? ;
A = imp(neg(q),true) ? ;
A = neg(q) ? ;
A = q ? ;
A = true ? ;
no
  • subformula述語の第1引数を変数Aとして実行すると, 第2引数の部分論理式をすべて求めることができる.
  • 表示された解に対してセミコロン (;) を入力すると, Prolog処理系はバックトラックを行い他の解を出力する. 他の解が存在しなければ no が表示される.

Author: 田村直之

Date: 2011年度前期

HTML generated by org-mode 7.3 in emacs 23