; by Alex Klinkhamer  (:handle grencez)
; Update: 2008.07.12
;
;  Legal info:
; You may exploit this code,
;    and it may exploit you.
; I am not responsible for either.

;;; Show binary representation,
;;; used only in debugging.
(defun showbits (x)
  (format t "~%~D: ~:*~B" x) x)

;;; Take a list of premises and check if
;;; the conclusion can be logically derived 
;;; ... return true or false accordingly
(defun verify-argument
  (premises conclusion &aux vars var-possi
            (var-count -1) (len 1))
  (labels
    ;V Acknowledge symbol, return its index in /vars/  V
    ;V Add the symbol to /vars/ if needed, doubling    V
    ;V all previously existing symbols' truth tables'  V
    ;V sizes/possibilities. Though every symbol has    V
    ;V two possible states (true or false), the        V
    ;V addition of a new variable doubles the possible V
    ;V truth combinations in the system.               V
    ((ratify-symbol
       (x &aux (index (position x vars)))
       (if index (- var-count index)
         (loop for b in var-possi
               collect (logior (ash b len) b) into tmp-possi
               finally
               (setf var-possi
                     (if var-possi
                       (cons (ash (logior b (ash b -1)) len)
                             tmp-possi) '(2)) len (* 2 len))
               (push x vars) (return (incf var-count)))))
     ;V Return copy of logic argument list, /lis/,          V
     ;V replacing normal operation names with bitwise ones, V
     ;V and each symbol name with its position in /vars/    V
     (map-for-bits
       (lis)
       (if (atom lis) (ratify-symbol lis)
         (cons (ecase (car lis) (not 'lognot) (and 'logand)
                 (or 'logior) (if 'logorc1) (equiv 'logeqv))
               (mapcar #'map-for-bits (cdr lis)))))
     ;V Return a copy of logic argument list (of the   V
     ;V type returned by map-for-bits), replacing      V
     ;V symbol indices with corresponding truth tables V
     ;V (numbers holding true/false with bits).        V
     (args-to-bits
       (lis)
       (if (atom lis) (svref var-possi lis)
         (cons (car lis) (mapcar #'args-to-bits (cdr lis)))))
     ;V Call eval on the args-to-bits modified list.V
     (eval-truths (lis) (eval (args-to-bits lis))))
    (setq premises (map-for-bits (cons 'and premises))
          conclusion (map-for-bits conclusion)
          var-possi
          (make-array (1+ var-count)
                      :initial-contents (nreverse var-possi)
                      :element-type 'integer))
    ;V Check if all valid truth combinations for premises V
    ;V also lead to the conclusion's truth                V
    (zerop (logand (eval-truths premises)
                   (lognot (eval-truths conclusion))))))


;; example calls, obviously there is no output
;; when run, but they return true because
;; the arguments are valid

(verify-argument
  ; Premise:
  ; 1. (R and S) if and only if (G and H)
  '((equiv (and r s) (and g h))
    ; 2. if R then S
    (if r s)
    ; 3. if H then G
    (if h g))
  ; Conclusion:
  ; R if and only if H
  '(equiv r h))

(verify-argument
  ; Premise:
  ; 1. if A then [if (N or not N) then (S or T)]
  '((if a (if (or n (not n)) (or s t)))
    ; 2. if T then not (F or not F)
    (if t (not (or f (not f)))))
  ; Conclusion:
  ; if A then S
  '(if a s))