;; lisp_sample.ss
;;      LISPサンプルプログラム ： 命題の証明
;;      2008 Nov.  水野嘉明
;;      【「コンパイラのうちとそと」（島内剛一他 共立出版）所載の
;;         LISPプログラムを、水野がScheme用に移植】

(define prove (lambda (f)
    (test (list (normalize f)) () () ) ))

(define normalize (lambda (f)
    (cond ((atom? f) f)
        ((eq? (car f) (quote and))
            (list (quote and)
                (normalize (cadr f))
                (normalize (caddr f)) ))
        ((eq? (car f) (quote or))
            (list (quote or)
                (normalize (cadr f))
                (normalize (caddr f)) ))
        ((eq? (car f) (quote imply))
            (list (quote or)
                (negate (cadr f))
                (normalize (caddr f)) ))
        ((eq? (car f)(quote not))
            (negate (cadr f)) )             )))

(define negate (lambda (f)
    (cond ((atom? f) (list (quote neg) f))
        ((eq? (car f) (quote and))
            (list (quote or)
                (negate (cadr f))
                (negate(caddr f)) ))
        ((eq? (car f) (quote or))
            (list (quote and)
                (negate (cadr f))
                (negate (caddr f)) ))
        ((eq? (car f)(quote imply))
            (list (quote and)
                (normalize (cadr f))
                (negate(caddr f)) ))
        ((eq? (car f) (quote not))
            (normalize (cadr f)) )          )))

(define test (lambda (s p n)
    (cond ((null? s) () )
        (else (reduce (car s) (cdr s) p n))) ))

(define reduce (lambda (f s p n)
    (cond ((atom? f)
            (cond ((member f n) #t)
                (else (test s (cons f p) n))))
        ((eq? (car f) (quote neg))
            (cond ((member f p) #t)
            (else (test s p (cons (cadr f) n)))))
        ((eq? (car f) (quote and))
            (and (reduce (cadr f) s p n)
                (reduce (caddr f)s p n)))
        ((eq? (car f) (quote or))
            (reduce (cadr f) (cons (caddr f) s) p n)))))

(define atom? (lambda (x)
    (or (symbol? x) (number? x) (null? x)) ))


;;
;;  A ∨ (B ∧ C) ⊃ （A ∨ B) ∧ (A ∨ C) を証明
;;
(prove '(imply (or a (and b c))
         (and (or a b) (or a c))) )

;;
;;  A ∧ (A ⊃ B) ⊃  B を証明
;;
(prove '(imply (and a (imply a b)) b) )