Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
#lang racket
(require rackunit
(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)))
"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))))
"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))))
#lang racket
(provide resolve
(define (member? item seq)
(sequence-ormap (lambda (x)
(equal? item x))
(define (invert x)
(if (list? x) (cadr x)
(list 'not x)))
(define (combine a l)
[(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)
[(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))
[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))])
[(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))
[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)))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment