; Logic.scm (define (dec-to-bin n) (define (aux q) (if (= q 0) '() (cons (remainder q 2) (aux (quotient q 2))))) (reverse (aux n))) (define (to-bool lst) (map (lambda (e) (if (= e '0) #f #t)) lst)) (define (fill-up lst l char) (if (< (length lst) l) (fill-up (cons char lst) l char) lst)) (define (truth-table f num-vars) (define (make-row i) (list (append (fill-up (dec-to-bin i) num-vars '0) (list (apply f (fill-up (to-bool (dec-to-bin i)) num-vars '#f)))))) (define (iterate i max result-list) (if (<> (length (filter (lambda (phi) (equal? phi e)) lst)) 0)) (define (taut? f num-vars) (not (contains? (truth-list f num-vars) '#f))) (define (sat? f num-vars) (contains? (truth-list f num-vars) '#t)) (define (display-form-type f num-vars) (display "Erfuellbar: ") (display (sat? f num-vars)) (newline) (display "Tautologie: ") (display (taut? f num-vars)) (newline))
; Solution to "Logic for Computer Scientists" Exercise 4 a) (define (solve form num-vars) (display-truth-table form num-vars) (display-form-type form num-vars))
(define (impl a b) (or (not a) b)) ; ==> a -> b (define (equiv a b) (equal? a b)) ; ==> a <-> b
; Form 1) (display "FORM 1 ===")(newline) (define form1 (lambda (x y z) (equiv (impl (and x y) z) (impl x (impl y z))))) (solve form1 3)
; Form 2) (display "FORM 2 ===")(newline) (define form2 (lambda (x y) (equiv (equiv (equiv (equiv x y) x) y) x))) (solve form2 2)
; Form 3) (display "FORM 3 ===")(newline) (define form3 (lambda (x y z w) (impl (not (impl (impl x y) (impl (impl x z) (impl x (and y z))))) (equiv (and x (not w)) (impl y (or x w)))))) (solve form3 4)
|
0 Comments:
Post a Comment