Schemeの課題(2012) --- (7b)

Copyright(C)2006 by 桜川貴司

命題論理の論理式の標準形

2値 命題論理 の論理式には,標準形がある. ここでは,そのうちのひとつ,論理和標準形を求めるプログラムを書いてみるこ とにする. (上のリンク先はWikipediaです).

論理和標準形を求める過程は,通常次のような手順を経る. ただし,∧と∨が本来は引数2つのオペレータであるのを, 結合法則と交換法則が成り立つため,n-aryのオペレータとして扱う. この場合,引数0個の∧は真,引数0個の∨は偽,として扱う.

この時点で,トップレベルが∨,2レベル目が∧,3レベル目が 命題変数,定数かその否定となる. その後,以下を繰り返し行って単純化を行う. 単純化は,行えなくなるまで,あるいはそれが保証されるまで繰り返すことになる.

2つ目の単純化では,並び順を変えられることに注意すること.

別のアルゴリズムとして以下のようなものも考えられる.

この時点で,やはりトップレベルが∨,2レベル目が∧,3レベル目が 命題変数,定数かその否定となる. その後,上に書かれた単純化をを繰り返し行う.



[kadaib28]

2値命題論理の論理式の論理和標準形を求めるプログラムを記述せよ. 命題定数としては#t,#fをそれぞれ真,偽として扱い, 命題変数は任意のシンボルで表すとする. 入力の論理式は以下のように定義される.

ここでは,標準形とは以下のような論理式とする.

ヒント:このページの上の方に書いてある, 標準形を求めるためのどちらかの方法に従ってプログラムを書けばよい. ただし,最初のアルゴリズムの方が効率が良い場合が多いであろう. 効率が良くなるようにアルゴリズムを変形できればもっと良い.

もう一つの方法として, 最初に論理式から命題変数を抜き出してリストを作り, それらから考えられる限りの標準形を生成して, 元の論理式と同等かどうかを一つ一つ確かめてゆくアルゴリズムが考えられる (上の条件を満たすような,一定個数の命題変数を持つ論理式は 有限個しかないために,停止性は保証される). このアルゴリズムによっても問題を解くことができるが, 効率が良くないであろうと思われる.

(この課題は, 命題論理の論理式の 充足可能性問題 を拡張したものとなっていて,NP困難であり, そのことからも多項式時間ではおそらく解けないことがすぐにわかる. したがって計算量の理論で通常いわれているいい方をすると, 問題自体が実用的に解ける問題ではないということになる. しかし,それでも小さい論理式については計算機で実際に解を求めることができるし, アルゴリズムによる計算量の差も当然あり得る.)

動作例:

	==>> (and-or-normal-form '(and (or a b) (or c d)))
	(or (and a c) (and a d) (and b c) (and b d))
	==>> (and-or-normal-form '(and (or) (or c d)))
	#f
	==>> (and-or-normal-form '(or (and) (or c d)))
	#t
	==>> (and-or-normal-form '(and (and a b))
	(and a b)
	

自動証明に興味がある人は, Resolution Presburger Arithmetic について調べてみるとよい.