;;;; Propositional Calculus
;;;;
;;;; File:         propositional-calculus.lsp
;;;; Author:       <your name> (<your e-mail address>)
;;;; Version:      1

;; In the following it is assumed that the symbols T,
;; F, and NIL are NEVER used as variables.
;;
;; It is also assumed that DNF formula do NOT contain
;; the constants T or F.
;;
;; The IMPLIES operation is NOT handled by this code.
;;
;; Most of the functions below are defined only on
;; input obeying particular assumptions.  None of these
;; functions makes any attempt to check for inputs that
;; do not obey the required assumptions.  E.g. many
;; functions work only on wff, and some only on DNF wff
;; or DNF clauses.


;; Functions to make code more readable.
;;
(defun op (e) (car e))
(defun arg1 (e) (cadr e))
(defun arg2 (e) (caddr e))
;;
(defun is-not-exp (e) (and (consp e) (eql 'not (op e))))
(defun is-and-exp (e) (and (consp e) (eql 'and (op e))))
(defun is-or-exp (e) (and (consp e) (eql 'or (op e))))



;; Evaluate a well formed formula e that contains NO
;; variables.
;;
;; RR: 
;;     
;;     
;;     
;;
(defun evaluate (e)
  )


;; Determine whether an s-expression e is a well formed
;; formula of the propositional calculus with constants.
;; Both constants and variables may appear in e, but NIL
;; may not.  Assumes e does NOT contain any dotted
;; sublists.
;;
;; RR: (wff? 's) ===> (not (eql 'nil 's))  s is a symbol
;;     (wff? `(not e1)) ===> (wff? e1)
;;     (wff? `(and e1 e2)) ===>
;;	   (and (wff? (arg1 e)) (wff? (arg2 e)))
;;     (wff? `(or e1 e2)) ===>
;;	   (and (wff? (arg1 e)) (wff? (arg2 e)))
;;     (wff? `e) ===> false	if above not applicable
;;
(defun wff? (e)
  (cond
   ((symbolp e)
    (not (eql 'nil e)))
   ((and (is-not-exp e) (= 2 (length e)))
    (wff? (arg1 e)))
   ((and (is-and-exp e) (= 3 (length e)))
    (and (wff? (arg1 e))
	 (wff? (arg2 e))))
   ((and (is-or-exp e) (= 3 (length e)))
    (and (wff? (arg1 e))
	 (wff? (arg2 e))))))



;; Substitute in a wff e for the variables in an
;; assignment a.  The name ASSIGN is chosen for
;; this function because COMMONLISP already has
;; a function named SUBSTITUTE.
;;
;; RR: (assign 'a 't) ===> 't
;;     (assign 'a 'f) ===> 'f
;;     (assign 'a 'v)
;;	   ===> (second (assoc 'v 'a))	if this is not
;;						nil
;;	   ===> 'v			otherwise
;;     (assign 'a '(not e))
;;	   ===> `(not ,(assign 'a 'e))
;;     (assign 'a '(and e1 e2))
;;	   ===> `(and ,(assign 'a 'e1)
;;		      ,(assign 'a 'e2))
;;     (assign 'a '(or e1 e2))
;;	   ===> `(or ,(assign 'a 'e1)
;;		     ,(assign 'a 'e2))
;;
(defun assign (a e)
  (cond
   ((eql 't e)
    't)
   ((eql 'f e)
    'f)
   ((symbolp e)
    (or (second (assoc e a)) e))
   ((is-not-exp e)
    `(not ,(assign a (arg1 e))))
   ((is-and-exp e)
    `(and ,(assign a (arg1 e))
	  ,(assign a (arg2 e))))
   ((is-or-exp e)
    `(or ,(assign a (arg1 e))
	 ,(assign a (arg2 e))))))



;; Given a wff e return any one variable that is in it.
;; Return NIL if there are no variables.
;;
;; RR: (one-variable 'f) ===> nil
;;     (one-variable 't) ===> nil
;;     (one-variable 'v) ===> 'v	v is a variable
;;     (one-variable '(not e)) ===> (one-variable 'e)
;;     (one-variable '(and e1 e2))
;;	   ===> (or (one-variable 'e1)
;;		    (one-variable 'e2))
;;     (one-variable '(or e1 e2))
;;	   ===> (or (one-variable 'e1)
;;		    (one-variable 'e2))
;;
(defun one-variable (e)
  (cond
   ((eql 't e)
    nil)
   ((eql 'f e)
    nil)
   ((symbolp e)
    e)
   ((is-not-exp e)
    (one-variable (arg1 e)))
   (t
    (or (one-variable (arg1 e))
	(one-variable (arg2 e))))))



;; Determine whether a wff e is a theorem by evaluating
;; its truth table.  Return non-nil if e is a theorem,
;; and nil if e is not a theorem.
;;
;; RR: 
;;     
;;     
;;
(defun theorem?-1 (e)
  )



;; Trace facility for rewrites:
;;
(defvar *trace* nil)     ; True to print trace,
			 ; false not to.

;; Call when rewriting an original equation to a new
;; rewritten equation.
;;
(defun rr (original rewrite)
  (cond (*trace*
	 (fresh-line)
	 (princ `(,original => ,rewrite))
	 (fresh-line))))



;; Compute the DNF of a wff e where e is assumed to
;; be either the AND of two already-DNF arguments,
;; or the OR of two already-DNF arguments.
;;
;; RR: 
;;     
;;     
;;     
;;
(defun dnf-distribute (e)
  )



;; Compute the DNF of a wff.  It is assumed that the
;; wff does NOT contain the constants T or F.
;;
;; RR: 
;;     
;;     
;;     
;;
(defun dnf (e)
  )



;; Given a DNF wff e, return the literals in it.  The
;; returned list of literals contains no duplicates.
;;
;; RR: (literals 's) ===> '(s)		s is a symbol
;;     (literals '(not s)) ===> '((not s))
;;     (literals '(and e1 e2))
;;	   ===> (union (literals 'e1) (literals 'e2))
;;     (literals '(or e1 e2))
;;	   ===> (union (literals 'e1) (literals 'e2))
;;
(defun literals (e)
  (cond
   ((symbolp e)
    `(,e))
   ((is-not-exp e)
    `(,e))
   (t
    (union (literals (arg1 e))
	   (literals (arg2 e)) :test #'equal))))


;; Given a literal return the literal that is its
;; negation.
;;
;; RR: (negate 's) ===> '(not s)	s is a symbol
;;     (negate '(not s)) ===> 's
;;
(defun negate (literal)
  (cond
   ((is-not-exp literal)
    (arg1 literal))
   (t
    `(not ,literal))))



;; Given a DNF clause, return true if and only if the
;; clause is unsatisfiable.  This later is true if and
;; only if the list of literals in the clause contains
;; both a variable and its negation.
;;
;; RR: (unsatisfiable-dnf-clause c)
;;	 ===> (unsatisfiable-dnf-clause c (literals c))
;;     (unsatisfiable-dnf-clause c '()) ===> nil
;;     (unsatisfiable-dnf-clause c '(x . y))
;;	 ===> true      if (member (negate 'x) 'y)
;;	 ===> (unsatisfiable-dnf-clause c 'y)
;;			otherwise
;;
(defun unsatisfiable-dnf-clause
      (c &optional (literal-list (literals c)))
  (cond
   ((null literal-list)
    nil)
   ((member (negate (first literal-list))
	    (rest literal-list) :test #'equal)
    t)
   (t
    (unsatisfiable-dnf-clause c (rest literal-list)))))



;; Given a DNF wff, return true if and only if it is
;; unsatisfiable.
;;
;; RR: (unsatisfiable-dnf '(or e1 e2))
;;	   ===> (and (unsatisfiable-dnf 'e1)
;;	             (unsatisfiable-dnf 'e2))
;;     (unsatisfiable-dnf 'e)
;;	   ===> (unsatisfiable-dnf-clause 'e)
;;			if above not applicable
;;
(defun unsatisfiable-dnf (e)
  (cond
   ((is-or-exp e)
    (and (unsatisfiable-dnf (arg1 e))
	 (unsatisfiable-dnf (arg2 e))))
   (t
    (unsatisfiable-dnf-clause e))))



;; Return true if a wff e is a theorem, using the
;; method of determining if the DNF of (not e) is
;; unsatisfiable.
;;
;; RR: 
;;
(defun theorem?-2 (e)
  )