Skip to content

Instantly share code, notes, and snippets.

# heidisu/prover-test.rkt Last active Jan 23, 2019

 #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))))
 #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)))
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.