ソフトウェア科学特論: Prologと命題論理
1 概要
Prologの概要等については,以下のWebページを参照のこと.
1.1 注意
本Webページ(およびPDF)の作成には Emacs org-mode を用いており, 数式等の表示は MathJax を用いています. IEでは正しく表示されないことがあるため, Firefox, Safari等のWebブラウザでJavaScriptを有効にしてお使いください. また org-info.js を利用しており, 「m」キーをタイプするとinfoモードでの表示になります. 利用できるショートカットは「?」で表示されます.
2 インストール
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 が表示される.