|
#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))) |