Propositional logic

propositional.lisp

(in-package :cl-user)

(definfix or :precedence 50)
(definfix and :precedence 40)
(definfix not :precedence 30)
(definfix => :precedence 60)
(definfix <=> :precedence 70)

(defun implies (a b)
  (or (not a) b))

(defun equivalent (a b)
  (or (and a b)
      (not (or a b))))


(defmacro nfxpr (&rest s)
  (list 'quote (nfx-impl s)))

(defun evaluate-expression (expr bindings)
  "Evaluate expression in propositional logic using the assoc-list of
binding given in BINDINGS. Operators in EXPR are: AND, OR, NOT,
IMPLIES, EQUIVALENT."
  (if (listp expr)
      (case (first expr)
        (and (and (evaluate-expression (second expr) bindings)
                   (evaluate-expression (third expr) bindings)))
        (or (or (evaluate-expression (second expr) bindings)
                 (evaluate-expression (third expr) bindings)))
        (not (not (evaluate-expression (second expr) bindings)))
        (=> (implies (evaluate-expression (second expr) bindings)
                           (evaluate-expression (third expr) bindings)))
        (<=> (evaluate-expression (evaluate-expression (second expr) bindings)
                                          (evaluate-expression (third expr) bindings)))
        (t (error "Unknown operator ~A" (first expr))))
      (cdr (assoc expr bindings))))

(defun collect-vars (expr)
  "Returns the list of all variables in EXPR."
  (let ((res (list)))
    (cond ((listp expr)
           (dolist (x (mapcan #'collect-vars (cdr expr)))
             (pushnew x res)))
          ((null expr))
          ((equal expr t))
          ((symbolp expr)
           (pushnew expr res)))
    (sort res #'string< :key #'symbol-name)))

(defun all-combinations (vars)
  "Returns a list of assoc lists of all the possible bindings for VARS."
  (loop for i from 0 below (expt 2 (length vars))
     collect (loop for var in vars
                for j from 0
                collect (cons var (= (ldb (byte 1 j) i) 1)))))

(defun truth-table (expr)
  "Calculates the truth table for EXPR."
  (let* ((vars (collect-vars expr))
         (combinations (all-combinations vars)))
    (loop for bindings in combinations
         collect (list bindings (evaluate-expression expr bindings)))))

(defun format-table (expr)
  "Prints the truth table for EXPR."
  (let* ((table (truth-table (nfx-impl expr)))
         (row (first table))
         (vars (first row)))
    (format t "~{~6@a~^ |~}" vars)
    (format t " || ~d~%" expr)
    (format t "-------------------------------------------------~%")
    (dolist (row table)
      (format t "~{~6@a~^ |~}" (mapcar #'(lambda (x) (if (cdr x) "TRUE" "FALSE")) (first row)))
      (format t " || ~d~%" (if (second row) "TRUE" "FALSE")))))

(defun equivalent-exprs (expr1 expr2)
  (let* ((vars (collect-vars (nfx-impl expr1)))
         (bindings (all-combinations vars)))
    (every #'(lambda (binding)
               (eql (evaluate-expression (nfx-impl expr1) binding)
                    (evaluate-expression (nfx-impl expr2) binding)))
           bindings)))

CL-USER> (format-table '(a => b))
   (A) |   (B) || (A => B)
-------------------------------------------------
 FALSE | FALSE || TRUE
  TRUE | FALSE || FALSE
 FALSE |  TRUE || TRUE
  TRUE |  TRUE || TRUE
NIL
CL-USER> (equivalent-exprs '(a => b) '(a or (not b)))
NIL
CL-USER> (equivalent-exprs '(a => b) '(b or (not a)))
T