#lang scheme

;; Implement resolution for propositional logic
;;
;; written by mike slattery - feb 2010
;; modified mcs - mar 2010
;; The function inconsistent? added to do
;; "proofs" easily.  If you add the negation of a
;; sentence s to
;; the knowledge base (KB) and find the result
;; is inconsistent, then you know s follows
;; logically from the KB.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (resolve-unit u lst)
  ;; given a literal u and a list of literals
  ;; return lst minus -u if -u in lst
  ;; otherwise, add u to the *set* lst and return
  (cond ((null? lst) (list u))
        ((member u lst) lst)
        (else (let ((not-u (negate-unit u)))
                   (if (member not-u lst)
                       (remove not-u lst)
                       (cons u lst))))
   ))
(define (negate-unit u)
  (if (list? u) (cadr u)
      (list 'not u)
      ))
(define (contains-negative? u lst)
  ;; u is a literal, lst is a list of literals
  ;; return true if lst contains the negative of
  ;; u
  (list? (member (negate-unit u) lst))
  )
(define (count-complements lst1 lst2)
  ;; return number of pairs of negatives
  (cond ((null? lst1) 0)
        ((contains-negative? (car lst1) lst2)
            (+ 1 (count-complements (cdr lst1) lst2)))
        (else (count-complements (cdr lst1) lst2))
  ))
(define (resolve lst1 lst2)
  (cond ((null? lst1) lst2)
        (else (resolve-unit (car lst1)
                            (resolve (cdr lst1) lst2)))
  ))
(define (canonical lst)
  (sort lst string<? #:key (lambda (x) (format "~a" x)))
  )
(define (add-clause c kb)
  ; add canonical form of c to kb if it's not
  ; already there. return updated kb
  (let ((cc (canonical c)))
    (if (member cc kb)
        kb
        (cons cc kb))
    ))

(define (all-pairs lst)
  ;; return a list of all pairs of elements
  ;; from lst
  (cond ((< (length lst) 2) '())
        (else (append
               (map (lambda (x) (list (car lst) x)) (cdr lst))
               (all-pairs (cdr lst))))
        ))
(define (good-pair? pair)
  ;; given a pair of clauses,
  ;; return true if the pair has one set
  ;; of complementary literals
  (= 1 (count-complements (car pair) (cadr pair)))
  )
(define (resolve-pairs pairs lst)
  ;; add the resolutions of the pairs in pairs
  ;; to the list lst without duplication
  (if (null? pairs) lst
      (let ((pair (car pairs)))
        (add-clause (resolve (car pair) (cadr pair))
                    (resolve-pairs (cdr pairs) lst)))
      ))
(define (resolve-all clauses)
  (let* ((pairs (all-pairs clauses))
         (goods (filter good-pair? pairs)))
  (resolve-pairs goods clauses))
  )

(define (inconsistent? clauses)
  (let ((size (length clauses)))
    (printf "Begin resolution of ~a clauses...\n" size)
    (incon-intern clauses 1 size)
 ))
  
(define (incon-intern clauses step size)
  (let* ((new-clauses (resolve-all clauses))
         (new-size (length new-clauses)))
    (printf "Step ~a: ~a clauses\n" step new-size)
    (cond ((list? (member '() new-clauses)) #t)
          ((= size new-size) #f)
          (else (incon-intern new-clauses (+ step 1) new-size))
     )))
        
    
  
(define cl2 '(((not P) Q)(P)((not Q))))

(define rules '(((not P11))
                ((not B11) P12 P21)
                    ((not P12) B11)
                    ((not P21) B11)
                ((not B21) P11 P22 P31)
                    ((not P11) B21)
                    ((not P22) B21)
                    ((not P31) B21)
                ((not B11))
                (B21)))