prover-test.rkt

#lang racket

(require rackunit
         "prover.rkt")

(check-equal? (resolve '(or P) '(or Q)) 'no-resolvent)
(check-equal? (resolve '(or P) '(or (not P))) '(or))
(check-equal? (resolve '(or P (not Q)) '(or Q (not R))) '(or P (not R)))

(test-case
 "prove true"
 (let ([premise '(and (or Q (not P))
                      (or R (not Q))
                      (or S (not R))
                      (or (not U) (not S)))]
       [negation '(and (or P) (or U))])
   (check-true (prove premise negation))))

(test-case
 "prove false"
 (let ([premise '(and (or Q (not P))
                      (or R (not Q))
                      (or S (not R))
                      (or (not U) (not S)))]
       [negation '(and (or P) (or S))])
   (check-false (prove premise negation))))

prover.rkt

#lang racket

(provide resolve
         prove)

(define (member? item seq)
  (sequence-ormap (lambda (x)
                    (equal? item x))
                  seq))

(define (invert x)
  (if (list? x) (cadr x)
      (list 'not x)))

(define (combine a l)
  (cond
    [(null? l) '()]
    [(or (equal? a (car l))
         (equal? (invert a) (car l))
         (member? (car l) (cdr l))) (combine a (cdr l))]
    [else (cons (car l) (combine a (cdr l)))]))

(define (resolve x y)
  (letrec ([res (λ (rest-x rest-y)
                 (cond
                   [(null? rest-x) 'no-resolvent]
                   [(member? (invert (car rest-x)) rest-y) (cons 'or (combine (car rest-x) (append (cdr x) (cdr y))))]
                   [else (res (cdr rest-x) rest-y)]))])
          (res (cdr x) (cdr y))))

(define (display-clauses x y)
  (displayln (append '(the clause) (list x)))
  (displayln (append '(and the clause) (list y))))

(define (prove premise negation)
  (letrec ([try-next-remainder (λ (remainder clauses)
                     (cond [(null? remainder)
                            (displayln '(theorem not proved))
                            #f]
                           [else (try-next-resolvent (car remainder) (cdr remainder) remainder clauses)]))]
           [try-next-resolvent (λ (first rest remainder clauses)
                       (if (null? rest) (try-next-remainder (cdr remainder) clauses)
                       (let ([resolvent (resolve first (car rest))])
                         (cond
                           [(or (equal? resolvent 'no-resolvent)
                                (member? resolvent clauses)) (try-next-resolvent first (cdr rest) remainder clauses)]
                           [(null? (cdr resolvent)) (display-clauses first (car rest))
                                                    (displayln '(produce the empty resolvent))
                                                    (displayln '(theorem proved))
                                                    #t]
                           [else (display-clauses first (car rest))
                                 (displayln (append '(produce a resolvent:) (list resolvent)))
                                 (try-next-remainder (cons resolvent clauses) (cons resolvent clauses))]))))]
           [clauses (append (cdr premise) (cdr negation))])
    (try-next-remainder clauses clauses)))