FC2ブログ
--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

05.24
Fri
お久しぶりです。

久しぶりに広告がついてしまいました(ブログを一ヶ月更新せず放置すると広告が出現する)

いろいろと忙しくてブログ更新できませんでした.

さて、タイトルの通り論理式の充足可能性を判定する方法である

タブロー法をCommonLispでやってみました

タブロー法は、論理学を作るを読んでみてこのブログでも

何度か使っていましたがそれです。

それを述語論理用に書いたんですが、実は問題があって

そもそも一般に、与えられた任意の述語論理の式(の集合)に対して

いつでも充足可能か否かを判定できるアルゴリズムは存在しない事が

証明されています.これはタブローのアルゴリズムに限らずです。

え、だったらなんでプログラム書いたの(てかそもそも書けないでしょ)?って話になりますが、

いくつかの場合についてちゃんと判定できるのです

非常に分かりやすい資料を見つけたのでリンクをはりますね

タブローの信頼性

つまり、タブローに与えられる式が充足可能の場合に限ってのみ停止しなくなるようですね。

ってことは、矛盾してたらちゃんと矛盾してることは判定できるわけです.

論理学を作るからも引用しますと、こうあります

P189
PPLの場合、タブローは止まらなくなることがある。
しかし、いつでも判定を下せるということと、判定が下せた時に
その判定を信頼できるということは別問題。


そして、こうあります

P190
・タブローの構成が止まって判定がでたなら、その判定は信頼できる
・タブロー構成が終わらなくなってしまうのはテストにかけたΓが
 充足可能な式集合であった場合に限られる


ということで、まぁ予め充足不可能っぽいなーっていう式をわたしてやれば

いいってことですね!!(

ということでコードを貼ります。

lexpr

このブログにもコードを垂れ流そうと思います

続きをどうぞ


述語論理を表す文字列をとるわけではなく、

S式で表された述語論理の式をとります

で肝心の判定は、inferパッケージのsemantic-conseqで行えます

一引数目に前提となる式のリストを取り、

2つ目の引数に結論となる式をわたします。

論理式は

(量化子部分 母式)

で表されます

たとえば、

`(((,+FORALL+ x)) (,+IMPL+ (P x) (Q x)))

で、 ∀x.P(x)⊃Q(x) を表します

量化子や論理結合子はconstパッケージに定義されているものをつかわないと、動かなくなります

defpack.lisp

;;;; パッケージを依存関係を考えながら
;;;; 定義し読み込む. 


(in-package :common-lisp-user)
(defpackage :constant.lexpr
	(:use :common-lisp)
	(:nicknames :const)
	(:export 
		:+FORALL+   :+EXIST+	
		:+QUANT+    :+IMPL+
		:+NEG+      :+AND+
		:+OR+       :+EQL+
		:+OPRT+     :+OPERATORS+
		:+FORALL-S+ :+EXIST-S+
		:+IMPL-S+   :+NEG-S+
		:+AND-S+    :+OR-S+
		:+EQL-S+    :+STRING-EXPR+
		:+NW+       :+LB+
		:+RB+       :+SP+
		:+CM+       :+OPR-STRENGTH+))
(in-package :const)
(load "./const.lisp")


(in-package :common-lisp-user)
(defpackage :util.lexpr
	(:use :common-lisp :const)
	(:nicknames :util)
	(:export 
		:quantsp      :opr-str
		:predexprp    :str-app
		:str-cut      :literalp
		:backetp      :quantsexprp
		:preproc
		:regular
	))
(in-package :util)
(load "./util.lisp")

(in-package :common-lisp-user)
(defpackage :convert2string.lexpr
	(:use :common-lisp :const)
	(:nicknames :dump)
	(:export :lexpr->string :dump-lexpr))
(in-package :dump)
(load "./dump.lisp")

(in-package :common-lisp-user)
(defpackage :inference.lexpr 
	(:use :common-lisp :const)
	(:nicknames :infer)
	(:export :semantic-conseq))
(in-package :infer)
(load "./infer.lisp")



const.lisp

;;;; 定数の定義
;;;; どのパッケージからでも修飾子なしで使える(use-packageされる)


(defconstant +FORALL+ 'forall)
(defconstant +EXIST+  'exist)
(defconstant +QUANT+  `(,+EXIST+ ,+FORALL+))
(defconstant +IMPL+   '->)
(defconstant +NEG+    'n)
(defconstant +AND+    'a)
(defconstant +OR+     'o)
(defconstant +EQL+    '<->)
(defconstant +OPRT+   `(,+IMPL+ ,+NEG+ ,+AND+ ,+OR+ ,+EQL+))
(defconstant +OPERATORS+ (union +QUANT+ +OPRT+))

(defconstant +OPR-STRENGTH+
	`(
	 	(,+NEG+  . 1)
		(,+AND+  . 2)
		(,+OR+   . 2)
		(,+IMPL+ . 3)
		(,+EQL+  . 3)))


(defconstant +FORALL-S+ "∀")
(defconstant +EXIST-S+  "∃")
(defconstant +IMPL-S+   "⊃")
(defconstant +NEG-S+    "¬")
(defconstant +AND-S+    "∧")
(defconstant +OR-S+     "∨")
(defconstant +EQL-S+    "⇔")

(defconstant +STRING-EXPR+ 
	`(
		(,+EXIST+  . ,+EXIST-S+)
		(,+FORALL+ . ,+FORALL-S+)
		(,+IMPL+   . ,+IMPL-S+)
		(,+NEG+    . ,+NEG-S+)
		(,+AND+    . ,+AND-S+)
		(,+OR+     . ,+OR-S+)
		(,+EQL+    . ,+EQL-S+)))


(defconstant +NW+ "")
(defconstant +LB+ ")")
(defconstant +RB+ "(")
(defconstant +SP+ " ")
(defconstant +CM+ ",")




util.lisp

;;;; いろいろと役に立つちょっとした関数を定義
;;;; 一般的なものと論理式関係のものを定義


;;; 一般的に使う関数


;;; (1 2 3 4 5) -> Boolean
;;; リストの要素が全てある型であるか
(defun allfactor (fun x)
	(and (listp x) 
		(reduce 
			(lambda (x y) (and x (funcall fun y))) x :initial-value t)))


;;; "abc" "def" -> "abcdef"
(defun str-app (&rest main) 
	(reduce (lambda (x y) (concatenate 'string x y)) main :initial-value ""))


;;; "abcdefg," -> "abcdefg"
;;; 最後の文字列を落とす
(defun str-cut (x) (subseq x 0 (1- (length x))))


;;; 再帰的に要素を数えるだけ
(defun countr (factor lst &optional (test #'eq)) "FACTOR , (LST)"
	(cond 
		((null lst) 0)
		((listp (car lst)) (+ (countr factor (car lst)) (countr factor (cdr lst))))
		((funcall test (car lst) factor) (+ 1 (countr factor (cdr lst))))
		(t (countr factor (cdr lst)))))






;;; 論理式関連の関数



;;; forall -> "∀ "
;;; 論理結合子の文字列表現を得る
(defun opr-str (opr) (cdr (assoc opr +STRING-EXPR+)))


;;; (forall x) | (exist y) | (not (not (not (forall x)))) ... -> Boolean
;;; 量化子として正しかったら t を返す
(defun quantp (x)
	(and 
		(= (length x) 2)
		(cond 
			((eq (first x) +FORALL+) t)
			((eq (first x) +EXIST+) t)
			((eq (first x) +NEG+) (quantp (second x)))
			(t nil))))


;;; ((forall x) (not (exist y)) (not (not (forall z)))) | ... -> Boolean
;;; 量化子部分として正しかった t を返す
(defun quantsp (x)
	(and 
		(allfactor #'listp x)
		(reduce 
			(lambda (x y)
				(and x (quantp y))) x :initial-value t)))


;;; (P x y z) | (Q x (f y) z)... -> Boolean
;;; 述語論理の原子論理式なら t を返す. 
(defun predexprp (x)
	(and 
		(listp x) 
		(not (member (car x) +OPRT+))
		(reduce 
			(lambda (x y)
				(and x
					(if (symbolp y)
						t (predexprp y))))
			(cdr x) :initial-value t)))



;;; (P x) | (not (P x)) | (not (not (not (Q y)))) ... -> Boolean
;;; 原子論理式かその否定なら t を返す
(defun literalp (lexpr)
	(cond 
		((symbolp lexpr) nil)
		((quantsp (car lexpr)) nil)
		((predexprp lexpr) t)
		((eq (car lexpr) +NEG+) (literalp (second lexpr)))
		(t nil)))


;;; not -> 1
;;; 論理結合子の結合の強さをもとめる
(defun strength (opr)  (cdr (assoc opr +OPR-STRENGTH+)))


;;; (opr1 (opr2 ...) (opr2 ...) (opr2 ...))
;;; カッコをつけるべきか判定. 第一引数はopr1 第二引数はopr2
;;; 中身の結合子の方が弱かったらカッコをつける
(defun backetp (opr1 opr2)
	(>= (strength opr2) (strength opr1)))


;;; (((forall x) (exist y)) (-> (P x) (Q y))) -> Boolean
;;; 量化された論理式か否かを判定する
(defun quantsexprp (lexpr)
	;; (car lexpr) は量化部分か論理結合子になる
	(quantsp (car lexpr)))


;;; forall -> exist
;;; 量化子の否定した形の量化子を得る
(defun negquant (quant)
	(cond 
		((eq quant +FORALL+) +EXIST+)	
		((eq quant +EXIST+) +FORALL+)
		(t (error "undefined quantifire"))))

;;; 量化子つけるな
;;; 2n回の否定をとる かならず先頭は否定の式じゃないとだめ
(defun rid-even-neg (lexpr)
	(cond 
		((symbolp (second lexpr)) lexpr)	
		((not (eq +NEG+ (car (second lexpr)))) lexpr)
		(t (rid-even-neg (second (second lexpr))))))



;;; 含意を (or (not p) q) の形に変換する. 量化子つけるな
;;; (-> (P x) (Q x)) -> (or (not (P x)) (Q x))
(defun impl->or (lexpr)
	(destructuring-bind (opr p q) lexpr
		`(,+OR+ (,+NEG+ ,p) ,q)))


;;; 同値を含意のandに変換する. 量化子つけるな
;;; (<-> p q) -> (and (-> p q) (-> q p))
(defun eq->impl (lexpr)
	(destructuring-bind (opr p q) lexpr
		`(,+AND+ (,+IMPL+ ,p ,q) (,+IMPL+ ,q ,p))))


;;; 含意と同値の除去を再帰的に全て行う
;;; 量化子のついてるやつついてない奴どっちも
(defun rid-eq-impl (lexpr)
	;; (quants (->|and|or|<->|not ...))
	;; (->|and|or|<->|not ...)
	;(format t "ARG: ~A~%" lexpr)
	(destructuring-bind (head . tail) lexpr
		;; head は量化子部分か結合子
		;(format t "TAIL: ~A~%" tail)
		(cond 
			((quantsp head)
				;; head が量化子部分だったら
				;; 量化子部分そのまま
				(list head (rid-eq-impl (car tail))))
			;; こっちにきたら普通に結合子(か述語)
			((literalp lexpr) lexpr)
			((eq head +IMPL+) (cons +OR+ (mapcar #'rid-eq-impl (cdr (impl->or lexpr)))) )
			((eq head +EQL+)  (cons +AND+ (mapcar #'rid-eq-impl (cdr (eq->impl lexpr))))  )
			;; and と or と not
			(t (cons head (mapcar #'rid-eq-impl tail))))))


;;; 一つの量化子について否定を返す
;;; 但しnotがなければそのまま返す
;;; (forall x) -> (forall x)
;;; (not (exist x)) -> (forall x)
;;; (not (not (forall x))) -> (forall x) 
(defun contrquant (quant)
	(destructuring-bind (head snd) quant
		(cond 
			((not (eq head +NEG+)) 
				(values quant nil))
			(t 
				(let ((clean (rid-even-neg quant)))
					(if (not (eq (car clean) +NEG+))
						(values clean nil)
						(values 
							(list 
								(negquant (car (second clean))) 
								(second (second clean))) t)))))))


;;; rid-quants-neg のヘルパ関数
;;; 先頭の否定形を追加する
(defun rid-quants-neg-1 (quants)
	(cons (list +NEG+ (car quants)) (cdr quants)))


;;; 量化子部分をとって否定でひっくり返した量化子部分
;;; ((forall x) (exist y) (not (forall z)) (exist z)) -> ((forall x) (exist y) (exist z) (forall w))
(defun rid-quants-neg (quants)
	(if (null quants)
		nil
		(multiple-value-bind (quant flag) (contrquant (car quants))
			(if flag
				(cons quant 
					(rid-quants-neg 
						;; 量化子部分と母式部分を別で考えてるからいけないんだとおもう
						;; これは最後の量化子だった時の処理
						(if (null (cdr quants)) 
							nil 
							(rid-quants-neg-1 (cdr quants)))))
				(cons quant (rid-quants-neg (cdr quants)))))))



;;; 量化子中の否定を除去る. 量化子のついた述語論理式
;;; (((forall x) (not (exist y))) (P x y)) -> (((forall x) (forall y)) (not (P x y)))
(defun rid-quants-neg-lexpr (lexpr)
	(destructuring-bind (quants body) lexpr
		(let ((clean-quants (rid-quants-neg quants))
		      (cnt (countr +NEG+ quants)))
			(list clean-quants
				(if (oddp cnt)
					`(,+NEG+ ,body) body)))))


;;; 論理式の中の全ての述語にかかる否定を取り除く
(defun rid-qneg (lexpr)
	;(format t "LEXPR: ~A~%" lexpr)
	(destructuring-bind (head . tail) lexpr
		;; (not P)
		;; head := not
		;; tail := (P)
		(cond 
			((quantsp head)
				;; lexpr は量化子のついた式だ!
				(let ((clean (rid-quants-neg-lexpr lexpr)))
					(list (car clean) (rid-qneg (second clean)))))
			((literalp lexpr) lexpr)
			((and (eq +NEG+ head) (quantsp (caar tail)))
				;; when head is negation
				;; like (not (((forall x) (exist y)) A))
				;; head := not
				;; tail := ((((forall x) (exist y)) A))
				(let ((body (car tail)))
					(destructuring-bind (quants main) body
						;; quants := ((forall x) (exist y))
						;; main := A
						(rid-qneg 
							(list 
								(cons (list +NEG+ (car quants)) (cdr quants)) main)))))
			(t 
				;; (->|or|and|not ...)
				(cons head (mapcar #'rid-qneg tail))
			))))



;;; ドモルガンで除去できる形式の論理式であるか判定
;;; リスト以外くるわけない
;;; (not (and|or ...)) -> t
(defun demorganp (lexpr)
	(cond 
		((not (eq (car lexpr) +NEG+)) nil)
		((or (eq +AND+ (car (second lexpr))) (eq +OR+ (car (second lexpr)))) t)
		(t nil)))

;;; ドモルガンの時に否定された結合子を返す
;;; and -> or , or -> and
(defun negopr (opr)
	(cond
		((eq opr +AND+) +OR+)
		((eq opr +OR+) +AND+)
		(t (error "and or or must be required"))))

;;; 量化子のつかない論理式のドモルガンで除去る
;;; (not (and|or ...)) -> (and|or (not ) (not ) ...)
(defun demorgan (lexpr)
	(cond 
		((demorganp lexpr) 
			(destructuring-bind (neg (opr . tail)) lexpr
				;; neg := not
				;; opr := or | and
				;; tail := ((P x) (Q x) ...)
				(cons (negopr opr) (mapcar (lambda (x) (list +NEG+ x)) tail)))) (t lexpr)))


;;; 論理式から再帰的にドモルガンできるやつをしまくる
;;;  関数の形がrid-eql-implと統合するなり、抽象化したかったけど統合するのは無理だった
;;;  なぜなら, -> <-> を除去ると途中で not が出てきてしまってめんどいことになる
;;;  (((forall x)) (not (or (P x) (Q x)))) -> (((forall x)) (and (not (P x)) (not (Q x))))
(defun rid-demorgan (lexpr)
	;(format t "LEXPR: ~A~%" lexpr) 
	(destructuring-bind (head . tail) lexpr
		;(format t "HEAD: ~A~%TAIL: ~A~%" head tail)
		;; head := quants | opr
		;; tail ((not (P x) (Q x))) , ((-> (P x) (Q y)))
		(cond
			((quantsp head)
				(list head (rid-demorgan (car tail))))	
			;; こっちにきたら 普通に結合子とか 述語
			((literalp lexpr) lexpr)
			;; demorgan できるかたち
			((demorganp lexpr) 
				(let* ((clean (demorgan lexpr)) (opr (car clean)))
					(cons opr (mapcar #'rid-demorgan (cdr clean)))))
			(t 
				;;ドモルガンできない一般のかたち
				(cons (car lexpr) (mapcar #'rid-demorgan tail))))))


;;; 二重否定を再帰的に全て除去する
(defun rid-dn (lexpr)
	;(format t "LEXPR: ~A~%" lexpr) 
	(destructuring-bind (head . tail) lexpr
		;(format t "HEAD: ~A~%TAIL: ~A~%" head tail)
		(cond
			((quantsp head)
				(list head (rid-dn (car tail))))	
			;; こっちにきたら 普通に結合子とか 述語
			((eq +NEG+ head)
				(rid-even-neg lexpr))
			((literalp lexpr) lexpr)
			(t 
				;;先頭がnotでない一般のかたち
				(cons (car lexpr) (mapcar #'rid-dn tail))))))


;;; 論理式を綺麗にする
(defun regular-1 (lexpr)	
	(rid-qneg (rid-dn (rid-demorgan (rid-eq-impl (rid-qneg lexpr))))))


;;; reqular-1だけでは綺麗にならないので
;;; 繰り返すだけ. なんか効率悪いぞこれ
;;; 論理式の構造的にどの除去則をやった後にこれをやれば
;;; 必ず綺麗になるみたいなのないのかな
(defun regular (lexpr)
	(let ((clean (regular-1 lexpr)))
		(if (equal lexpr clean)
			lexpr
			(regular clean))))



;;; 論理式中の自由変数を返す
;;; regular されたものにして
;;; bound は量化子によって束縛されているもののリスト
;;; 関数記号とか考慮してない
;;; (((foall x) (exist y)) (-> (P x y) (Q a y))) -> (a)
(defun collect-free (lexpr &optional (bound nil))
	(destructuring-bind (head . tail) lexpr
		(cond 
			((quantsp head) 
				(collect-free 
					(car tail) 
					(append bound (mapcar (lambda (x) (second x)) head))))
			((literalp lexpr) 
				;; lexpr := (not (P x y))
				;; lexpr := (P x y)
				(if (eq +NEG+ head)
					(collect-free (car tail) bound)	
					(if (null bound) ;; 束縛変数のリストが0だったら
						tail 
						(reduce 
							(lambda (x y) 
								(if (null (member y bound))
									(cons y x) x)) tail :initial-value nil))))
			(t 
				;; それ以外の結合子
				;; (and|or|not|->|<-> ...)
				;; regular されてるから (and|or|not ...) のはずだけど
				(apply #'append (mapcar (lambda (x) (collect-free x bound)) tail))))))



;;; 論理式を正規化して自由変数のリストを二値で返す
(defun preproc (lexprs)
	(let ((clean (mapcar #'regular lexprs)))
		(values clean
			(reduce 
				#'union 
				(mapcar #'collect-free clean)
				:initial-value nil))))




dump.lisp

;;;; 述語論理式の内部表現を文字列にして返す関数を提供する
;;;;
;;;; - 論理式の再帰的定義 -
;;;;
;;;; def. 述語は任意の長さのシンボルで良い
;;;; 
;;;; def. 項は 任意の長さのシンボルで良い
;;;;
;;;; def. 任意の変数,定数は項である
;;;;
;;;; def. 1個以上の項をとる関数は項である
;;;;
;;;;
;;;; def. 1個以上の項をとる述語を原子論理式とする
;;;;  
;;;; def. Aを任意の論理式とする時
;;;; 	 (not A) 
;;;; 	 は論理式である
;;;;
;;;; def. A,Bを任意の論理式とする時
;;;; 	 (and A B) (OR A B) (-> A B) (<-> A B)
;;;; 	 は論理式である
;;;;
;;;; def. Aを任意の論理式とする時
;;;;      (((forall 変項)) A) (((exist 変項)) A)
;;;;      は論理式である
;;;;
;;;; ※ 上記の定義では多重量化な式も生成されるが
;;;;   推論の決定性の関係上MPLに限られる可能性がある
;;;;   但しdumpでは多重量化も許すことにする
;;;;   つまりdump自体は上の定義の完全な述語論理式を扱えることにする
;;;;
;;;; ((量化子1 量化子2 ...) 式)


;;; (forall x) -> ∀ x  (exist y) -> ∃ y  (not (not (forall x))) -> ¬ ¬ ∀ x
;;; 最も簡単なパターンの量化子の変換
(defun quant->string (quant)
	(let* ((head (car quant)) 
		   (tail (second quant)) 
		   (head-str (util:opr-str head)))
		;; head は forall exist not の何れか
		;; tail は x,y,z 等の変数か head が not の時は量化子
		(if (eq head +NEG+)
			(util:str-app head-str (quant->string tail))
			(util:str-app head-str (symbol-name tail)))))


;;; ((forall x) (not (exist y)) (forall z)) | ... -> "∀ x¬ ∃ y∀ z"
;;; 量化子部分だけを文字列にして返す
(defun quants->string (quants)
	(reduce 
		(lambda (x y)
			(util:str-app x (quant->string y))) 
			quants :initial-value ""))


;;; (P x y z) | ... -> "P(x,y,z)"  (Q x y (f z)) | ... -> "Q(x,y,f(z))"
;;; 述語論理の原子論理式を文字列にする
(defun predexpr->string (predexpr)
	(util:str-app
		(util:str-cut 
			(reduce 
				(lambda (x y)
					(util:str-app x 
						(if (symbolp y) (symbol-name y) (predexpr->string y)) ","))
				(cdr predexpr)
					:initial-value (util:str-app (symbol-name (car predexpr)) "("))) ")"))


;;; lexpr->string のヘルパ. 適切にカッコをつけるか判断する
(defun lexpr->string-1 (head lexpr)
	(let ((opr (car lexpr)))
		(cond 
			((util:quantsexprp lexpr) 
				;; 量化子のついた論理式はカッコをつけよう
				(util:str-app "(" (lexpr->string lexpr) ")"))
			((util:literalp lexpr)
				;; リテラルだったらそのままにしよう
				(lexpr->string lexpr))
			((util:backetp head opr) 
				;; backetp が t だったらカッコをつける 
				(util:str-app "(" (lexpr->string lexpr) ")"))
			(t (lexpr->string lexpr)))))


;;: (((forall x) (not (exist y))) (-> (P x) (Q y))) | ... -> "∀ x¬ ∃ y(P(x) -> Q(y))"
;;; 述語論理の式を受け取って文字列で返す
(defun lexpr->string (lexpr)
	(let ((head (first lexpr))) 		
		;; head は量化子部分もしくは not and or -> <-> P,Q.. の何れか
		(cond 
			((util:quantsp head)
				;; 量化子部分を文字列に直して、母式の文字列表現と連結 
				(util:str-app 
					(quants->string head) "." (lexpr->string (second lexpr))))
			((eq +NEG+ head)
				;; 演算子がNEGなら被演算子部分は必ず一つなので(second lexpr)
				;; はメインの論理式. bodyに束縛
				;; 演算子がなんであれリテラル以外は必ずカッコはつけるべき
				(let ((body (second lexpr)) (neg-str (util:opr-str +NEG+)))
					(cond
					 	((util:literalp body)
							;; リテラルならそのままnotをつけてよし
							(util:str-app neg-str (lexpr->string body)))
						((util:quantsp (car body))
							;; bodyに量化子がついてたときはそのままnotにしよう... うーんどうしよう悩み中
							(util:str-app neg-str  (lexpr->string body) ))
						(t 
							;; それ以外はかならずカッコにくるもう
							(util:str-app neg-str "(" (lexpr->string body) ")")))))
			((util:predexprp lexpr)
				;; 原子論理式を文字列に	
				(predexpr->string lexpr))	
			(t 
				;; 普通の論理結合子に関する変換
				(util:str-cut 
					(reduce 
						(lambda (x y)
							(util:str-app x 
								;; y は任意の論理式が入ってるので
								;; 述語論理の式の場合は無条件でカッコでくるむ
								;; backetp が t と言う場合もカッコでくるむ 	
								;; lexpr->string-1 がそれを判断
								(lexpr->string-1 head y)
								(util:opr-str head)))
						(cdr lexpr) :initial-value ""))))))


(defun dump-lexpr (lexpr &key (strm t) (template "~A~%"))
	(format strm template (lexpr->string lexpr)))



infer.lisp

;;;; 式集合 Γ から φ が意味論的帰結であるかを判定 Γ |= φ
;;;; 判定にはタブロー法を使う
;;;; Γ |= φ ならば Γ ∪  {¬ φ} |= 
;;;; 
;;;; - PROPOSITION  RULE -
;;;; 1. Depend clause (Γ) include φ and (not φ) then close branch
;;;; 2. Depend clause (Γ) include (or φ ψ)  then branch Γ ∪ {φ} and Γ ∪ {ψ} 
;;;; -3. Depend clause (Γ) include (-> φ ψ)  then branch Γ ∪ {¬ φ} and Γ ∪ {ψ}
;;;; 4. Depend clause (Γ) include (and φ ψ) then branch Γ ∪ {φ , ψ}
;;;;
;;;; - PREDICATE RULE -
;;;; 5. Depend clause (Γ) include (((forall x)) φ) then branch Γ ∪ {φ[α/x] , (((forall x)) φ)} 
;;;; 6. Depend clause (Γ) include (((exist x)) φ)  then branch Γ ∪ {φ[α/x]} * α mustn't use in depend clause
;;;; 
;;;; 
;;;; 述語論理の決定性の問題から、infer で使う述語論理式はMPLに限ろうと思う



;;;; ------------------------------------------------------------------
;;;; 方針
;;;; ①  util:rid-quants-neg-lexpr で量化子部分を綺麗にして
;;;; ②  util:rid-eq-implで同値と含意を除去る
;;;;
;;;; この時and or not だけを結合子として使うようになる
;;;;
;;;; ③  not が and , or にかからない様にドモルガンで変形する
;;;; ④  単一化とタブローのルールに従っていく
;;;; ------------------------------------------------------------------




;;; 量化子があるなら展開可能: unification
;;; 結合子が -> なら展開可能: (-> P Q)        => not P , Q
;;; 結合子が OR なら展開可能: (OR P Q ... Z)  => P , Q , ... Z
;;; 結合子が ANDなら展開可能: (AND P Q ... Z) => P Q ... Z
;;; 結合子が <->なら展開可能: (<-> P Q)       => (-> P Q) (-> Q P)
;;; リテラルであるなら展開不可能: (not (P x (f y z))) (P x) (Q x y (f z)) は展開不可能
;;; 
;;; 結合子が not で その次が -> OR AND <-> なら展開可能
;;; 但し展開しなければ行けない(not ...) に直接適用できる規則はない
;;;
;;; lexpr はタブロー展開規則を適用可能かどうか
;;; リテラルな論理式以外なら展開可能とする
(defun applyp (lexpr)
	(if (util:literalp lexpr) nil t))


;;; Qα.φ sym -> φ[sym / α]
;;; lexpr の外側の量化子をはがす. lexpr必ず量化子のついたもの
(defun unification (lexpr sym)
	;; lexpr は (((forall x) (exist y) (forall z)) (-> (P x) (and (Q y) (R z))))
	;; みたいになってる. それ以外はしらない
	(let* ((quants-part (car lexpr)) 
			(head-quant (car quants-part))
			(body-part  (second lexpr))
			(rplc (subst sym (second head-quant) body-part)))
			;; quants-partに量化子部分をもってくる
			;; head-quantに 一番先頭の量化子一個を取ってくる
			;; body-partに述語論理の式のメインの部分を持ってくる
			;; rplcは置換した式
			(if (= 1 (length quants-part))
				rplc
				(list (cdr quants-part) rplc))))


;;; {P(x) , ¬ Q(x) } -> Boolean
;;; 全ての論理式が展開不可能かどうか 全ての式がリテラルであるか否か  
(defun all-literalp (lexprs) 
	(every (lambda (x) (not (applyp (car x)))) lexprs))


;;; 全称量化な式は単一化しても残るので
;;; どのシンボルで単一化したかを記憶してリストをもたせる
;;; 用に変形する
;;; regular されていると仮定
;;; プレースホルダ的な感じでforall以外にもつけてしまう
(defun forall-init (lexprs)
	(mapcar (lambda (x) (list x nil)) lexprs))


;;; forall-initでくっつけられたゴミみたいなnilをとりのぞくだけ
(defun rid-init (lexprs) 
	(mapcar (lambda (x) (car x)) lexprs))


;;; {¬ P(x) P(x)} -> t
;;; φの否定の形の式はlexprsに含まれているか
;;; O(n^2)でうける
;;; (((forall x)) (P x)) と (((exist y)) (not (P y))) が矛盾したものと判断されないぞー
(defun opposp-1 (lexpr lexprs)
	(let ((neg  (util:regular `(,+NEG+ ,lexpr))))
		;; lexprs のメタ情報を落とす
		(if (member neg (rid-init lexprs) :test #'equal) t nil)))

;;; 自分と否定の形の式は含まれているかどうか
;;; α同値な式に対応しなきゃ...
;;; とおもったけど、普通に量化子は除去られるのでいっか
(defun closep (lexprs)
	;; (car x) 取るのは 論理式の本体を得るため
	(some (lambda (x) (opposp-1 (car x) lexprs)) lexprs))


;;; lexprs := {(∃ x(P(x) -> Q(x)) nil) ...} みたな形式から先頭が存在量化な
;;; やつだけあつめる.(default)
(defun collect-exist (lexprs &optional (quants +EXIST+))
		(remove-if-not
			(lambda (x)
				(let* ((lexpr (car x)) (head (car lexpr)))
					(if (util:quantsp head)
						(eq (caar head) quants) nil))) lexprs))


;;; 存在量化の式のリストをもらって
;;; gensymで単一化した式とそのシンボルのリストを二値で返す
;;; {(∃ x(P(x) -> Q(x)) nil) , (∃ x(P(x)∧ Q(x)) nil)} -> {(P(a)->Q(a) nil) , (P(b)∧ Q(b) nil)}
(defun uni-exist (e-lexprs)
	(let ((exist-sym 
			(loop for x from 0 upto (1- (length e-lexprs)) 
				collect (gensym "RID-EXIST-"))))
		(values 
			(map 'list 
				(lambda (expr sym) 
					(list (unification (car expr) sym)  nil)) 
				e-lexprs  exist-sym)  
			exist-sym)))


;;; 優先的にforallの除去をすべき式を降順に並べる
(defun sort-forall (forall-lexprs)
	(sort forall-lexprs (lambda (x y) (< (length (second x)) (length (second y))))))


;;; 量化子のついていない式を集める
(defun collect-nexpr (lexprs) 
	(remove-if
		(lambda (x)
			(util:quantsexprp (car x))) lexprs))


;;; (and|or p q r ...)みたいのを
;;; ((p nil) (q nil) (r nil) ...) にする
(defun split-sublexpr (lexpr)
	(mapcar (lambda (x) `(,x nil)) (cdr lexpr)))

;;; 量化子のついていない式で展開可能なものを集める
(defun select-normal (lexprs)	
	(find-if #'applyp lexprs))

;;; forall な式に使うべきシンボルを返す
(defun select-symbol (forall-usedsym usedsym)
	;; もしusedsymがnil だったら今までcontrap-mainを実行してて
	;; 一個も自由変数がないってことだから forall のためのシンボルはなるべく
	;; 使われてきた奴とかぶせる必要があるけど、致し方ない
	;; forall-usedsym は usedsym の部分集合
	(let ((tmp (set-difference usedsym forall-usedsym)))
		(cond 
			((null tmp)
				(values (gensym "RID-FORALL-") t))
			(t (values (car tmp) nil)))))

(defun debug-print (lexprs usedsym)
	(format t "LEXPRS-SIZE: ~A~%ALL-USED-SYM: ~A~%------------------------------------------~%" 
		(length lexprs) usedsym)
	(loop for lexpr in lexprs for cont from 1 upto (length lexprs)  do 
		(format t "~A. ~%ORIGINAL: ~A~%STRING: ~A~%USED-SYM: ~A~%" 
			cont lexpr (dump:lexpr->string (car lexpr)) (second lexpr)))
	(format t "------------------------------------------~%~%"))


;;; lexprs を構成する式の要素
;;; 1. 全称量化な式
;;; 2. 存在量化な式
;;; 3. 展開可能式 or and
;;; 4. リテラル
(defun contrap-main (lexprs usedsym &optional (trc nil))
	(when trc (debug-print lexprs usedsym))
	(cond
		;; 自分の否定の形の式が含まれていたら矛盾
		((closep lexprs) t)
		;; すべてがリテラルで上の条件に合致しない、つまり
		;; 全ての式が自分の否定の形を含まないなら
		;; これ以上つくす手段はないので矛盾していない
		((all-literalp lexprs) nil)
		(t
			;; ここのlet でlexprs を
			;; 構成する式を4種類(5)に分ける
			(let* ((falq-lexprs (sort-forall (collect-exist lexprs +FORALL+)))
					;; 全称量化な式	
				   (extq-lexprs (collect-exist lexprs +EXIST+))
				    ;; 存在量化な式
				   (nrml-lexprs (collect-nexpr lexprs))
				    ;; リテラルと展開可能式をあわせたやつ
				   (ltrl-lexprs (remove-if (lambda (x) (applyp (car x))) nrml-lexprs))
				    ;; リテラル. もうこいつはいじれない
				   (extb-lexprs (remove-if (lambda (x) (not (applyp (car x)))) nrml-lexprs)))
					(cond 
						((not (null extq-lexprs))
							;; 存在量化をぶっ潰すそしてまた回す
							(multiple-value-bind 
								(rid-extq-lexprs syms) 
								(uni-exist extq-lexprs)
								(contrap-main 
									(append 
										falq-lexprs 
										rid-extq-lexprs
										nrml-lexprs) (append syms usedsym) trc)))
						((not (null extb-lexprs))
							;; ここにきたなら 少なくとも extq-lexprs はnilのはず
							;; なぜなら上で徹底的に取り除かれるから
							(let* ((target (car extb-lexprs))
								   ;; 展開可能な式の一つを選ぶ
								   (other-extb-lexprs (cdr extb-lexprs))
								   ;; target 以外の展開可能式
								   (main   (car target))
								   ;; body となる部分を取り出す
								   (opr    (car main))
								   ;; body の結合子を取り出す
								   (next-base (append falq-lexprs ltrl-lexprs other-extb-lexprs)))
								   ;; forall literal targetでない展開可能式はそのままもちこす
								   (cond 
								   		((eq opr +AND+)
											(contrap-main 
												(append 
													(split-sublexpr main) next-base) usedsym trc ))
										((eq opr +OR+)
											(every 
												(lambda (x)
													(contrap-main 
														`(,@next-base ,x) usedsym trc ))
												(split-sublexpr main)))
										(t "undefined operator: ~A" opr))))
						((not (null falq-lexprs))
							(let*  ((target (car falq-lexprs)) 
									;; ターゲットとなる全称量化な式が入る
									;; (∀ xP(x) used)
								    (main (car target))
									;; 式自体を取り出す
									;; ∀ xP(x)
									(falq-usedsym (second target))
									;; 今までに使われたのを取り出す 
									;; used
									(other-falq-lexprs (cdr falq-lexprs)))
									;; その他の全称量化単一化可能式
								(multiple-value-bind (sym flag) (select-symbol falq-usedsym usedsym)
									(let*  ((bound  (cons sym falq-usedsym))
										   	(unifed (list (unification main sym) nil))
											(update (list main bound))
											(next `(,@other-falq-lexprs ,update ,unifed ,@nrml-lexprs)))
										(if flag
											(contrap-main next (cons sym usedsym) trc )
											(contrap-main next usedsym trc ))))))
						(t (error "unexpected error: ~A~%" lexprs)))))))


;;; contrap-main へのインターフェース
(defun contrap (lexprs &optional (trc nil))
	(multiple-value-bind 
		(clean-lexprs init-free-value) (util:preproc lexprs)
		(contrap-main (forall-init  clean-lexprs) init-free-value trc)))


;; lexpr は lexprs からの 意味論的帰結となるか
(defun semantic-conseq (lexprs lexpr &optional (trc nil))
	(contrap `(,@lexprs (,+NEG+ ,lexpr)) trc))

(defun check-contrap (lexprs)
	(format t "{")
	(mapc (lambda (x) (dump:dump-lexpr x :template "~A , ")) lexprs)
	(format t 
		(if (contrap lexprs t) "} is contradiction~%~%" "} is satisfiable~%~%")))




TESTER.lisp

(load "defpack.lisp")
(use-package :const)



;; ソクラテスは死ぬか?
(format t "~A~%"
	(infer:semantic-conseq
		`(
			(((,+FORALL+ x)) (,+IMPL+ (human x) (mortal x)))
			(human sokrates))
		'(mortal sokrates) ))


;; { ∀ x∀ y.(∃ zH(y , z)) ⊃  H(x , y) , H(a , b)} |= ∀ z∀ w.H(z , w)  ? -> t
;; 論理学を作る の練習問題73から
;; {人は,人を憎む人を憎む , aさんはbさんを憎む} |= 全ての人は全ての人を憎む
;; の例
(format t "~A~%" 
	(infer:semantic-conseq 
		`(
			(((,+FORALL+ x) (,+FORALL+ y)) (,+IMPL+ (((,+EXIST+ z)) (H y z))  (H x y)))
			(H a b))
		`(((,+FORALL+ z) (,+FORALL+ w))(H z w))))



;; 論理学を作るの練習問題32の(5)
(format t "~A~%"
	(infer:semantic-conseq 
		`(
			(((,+FORALL+ x)) (,+IMPL+ (A x) (B x)))
			(((,+FORALL+ x)) (,+IMPL+ (C x) (D x)))
			(((,+FORALL+ x)) (,+IMPL+ (E x) (F x)))
			(((,+FORALL+ x)) (,+IMPL+ (,+NEG+ (G x)) (,+NEG+ (H x))))
			(((,+FORALL+ x)) (,+IMPL+ (B x) (I x)))
			(((,+FORALL+ x)) (,+IMPL+ (,+NEG+ (A x)) (,+NEG+ (J x))))
			(((,+FORALL+ x)) (,+IMPL+ (K x) (,+NEG+ (D x))))
			(((,+FORALL+ x)) (,+IMPL+ (,+NEG+ (H x)) (,+NEG+ (I x))))
			(((,+FORALL+ x)) (,+IMPL+ (,+NEG+ (J x)) (E x)))
			(((,+FORALL+ x)) (,+IMPL+ (G x) (C x))))
		 `(((,+FORALL+ x)) (,+IMPL+ (K x) (F x)))))

スポンサーサイト
comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/170-2b6611e3
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。