3値論理

CommonLispにもML系Matchがないのか。

(in-package "ACL2")

(defun not-3 (x)
  (cond ((equal x "yes") "no")
        ((equal x "no") "yes")
        ((equal x "maybe") "maybe")))

(defun and-3 (x y)
  (cond ((and (equal x "yes") (equal y "yes")) "yes")
        ((and (equal x "yes") (equal y "no"))  "no")
        ((and (equal x "yes") (equal y "maybe")) "maybe")
        ((and (equal x "no") (equal y "yes")) "no")
        ((and (equal x "no") (equal y "no")) "no")
        ((and (equal x "no") (equal y "maybe")) "no")
        ((and (equal x "maybe") (equal y "yes")) "maybe")
        ((and (equal x "maybe") (equal y "no")) "no")
        ((and (equal x "maybe") (equal y "maybe")) "maybe")))

(defun or-3 (x y)
  (cond ((and (equal x "yes") (equal y "yes")) "yes")
        ((and (equal x "yes") (equal y "no"))  "yes")
        ((and (equal x "yes") (equal y "maybe")) "yes")
        ((and (equal x "no") (equal y "yes")) "yes")
        ((and (equal x "no") (equal y "no")) "no")
        ((and (equal x "no") (equal y "maybe")) "maybe")
        ((and (equal x "maybe") (equal y "yes")) "yes")
        ((and (equal x "maybe") (equal y "no")) "maybe")
        ((and (equal x "maybe") (equal y "maybe")) "maybe")))

(defthm and-3-comm
  (iff (and-3 x y) (and-3 y x)))

(defthm and-3-ldistr-or-3
  (iff (and-3 t (or-3 u v)) (or-3 (and-3 t u) (and-3 t v))))

(defthm and-3-rdistr-or-3
  (iff (and-3 (or-3 t u) v) (or-3 (and-3 t v) (and-3 u v))))

全部自動で証明までできてる。