;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; First-order logic duplicate clause check for lisp.
;
;	- The goal is to flag clauses that are definitely different,
;	  i.e., number of literals are different, or the set of predicates
;	  is different. In other words, some clauses that are different
;	  can be potentially flagged as not different, such as 
;	  P(X) and P(Socrates).
;
; Author: Yoonsuck Choe <choe(a)tamu.edu>.
;
; - Type in one chunk at a time to see what it does.
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; A simple theorem (at least in its form).
; Each clause consists of 
;	- clause number
;	- list of positive literals
;	- list of negative literals
(defvar dummy '(   	(1     ( (Q X) (P (A)) )     ( (R X) )    	)
		  	(2     ( (P X) (Q (A)) (S Y))     ( (R X) )     )
	       )
)

; Get the two clauses from the theorem.
(setq clause1 (first dummy))
(setq clause2 (second dummy))

; Get the two positive literal lists from the clauses.
(setq pos1 (second clause1))
(setq pos2 (second clause2))

; Get the two negative literal lists from the clauses.
(setq neg1 (third clause1))
(setq neg2 (third clause2))

; Extract the predicate names only
(setq pos1-predicates (mapcar #'car pos1))
(setq pos2-predicates (mapcar #'car pos2))
(setq neg1-predicates (mapcar #'car neg1))
(setq neg2-predicates (mapcar #'car neg2))

; Sort and compare 
; This function is inspired by Kevin Orb's example:
;  	http://www.csse.monash.edu.au/~korb/.
(defun sort-symbol (predicate-list)
   (sort predicate-list #'(lambda (a b) 
				(string< (symbol-name a) (symbol-name b))
   			  )
   )
)

; Check sort symbol function
(sort-symbol '(z x y a g b))

; Check for dupe
(equal (sort-symbol pos1-predicates) (sort-symbol pos2-predicates))
(equal (sort-symbol neg1-predicates) (sort-symbol neg2-predicates))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
;	Member function, which may come in handy
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Try out the following
(setq check-list '(a b c e g k l x z))

(member 'y check-list :test 'equal)
; returns: NIL

(member 'x check-list :test 'equal)
; returns: (X Z), i.e., something that's not NIL.

(member 'g check-list :test 'equal)
; returns: (G K L X Z), i.e., something that's not NIL.

; You can change 'equal at the end with an arbitrary function
; to use the (member ...) function more flexibly.