Advertisement
Guest User

Untitled

a guest
Apr 9th, 2020
168
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Racket 4.64 KB | None | 0 0
  1. #lang racket
  2.  
  3. (provide falsifiable-cnf?)
  4. (require "props.rkt")
  5.  
  6. (define (prop? f)
  7.   (or (var? f)
  8.       (and (neg? f)
  9.            (prop? (neg-subf f)))
  10.       (and (disj? f)
  11.            (prop? (disj-left f))
  12.            (prop? (disj-right f)))
  13.       (and (conj? f)
  14.            (prop? (conj-left f))
  15.            (prop? (conj-right f)))))
  16.  
  17. (define (lit-var f)
  18.   (cond [(var? f) f]
  19.         [(neg? f) (neg-subf f)]
  20.         [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)]))
  21.      
  22. (define (free-vars f)
  23.   (cond [(null? f) null]
  24.         [(var? f) (list f)]
  25.         [(neg? f) (free-vars (neg-subf f))]
  26.         [(conj? f) (append (free-vars (conj-left f))
  27.                            (free-vars (conj-right f)))]
  28.         [(disj? f) (append (free-vars (disj-left f))
  29.                            (free-vars (disj-right f)))]
  30.         [else (error "Zła formula -- FREE-VARS" f)]))
  31.  
  32. (define (gen-vals xs)
  33.   (if (null? xs)
  34.       (list null)
  35.       (let*
  36.           ((vss (gen-vals (cdr xs)))
  37.            (x (car xs))
  38.            (vst (map (λ (vs) (cons (list x true) vs)) vss))
  39.            (vsf (map (λ (vs) (cons (list x false) vs)) vss)))
  40.         (append vst vsf))))
  41.  
  42. (define (eval-formula f evaluation)
  43.   (cond [(var? f)
  44.          (let ((val (assoc f evaluation)))
  45.            (if (not val)
  46.                (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation)
  47.                (cadr val)))]
  48.         [(neg? f) (not (eval-formula (neg-subf f) evaluation))]
  49.         [(disj? f) (or (eval-formula (disj-left f) evaluation)
  50.                        (eval-formula (disj-right f) evaluation))]
  51.         [(conj? f) (and (eval-formula (conj-left f) evaluation)
  52.                         (eval-formula (conj-right f) evaluation))]
  53.         [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)]))
  54.  
  55. (define (falsifiable-eval? f)
  56.   (let* ((evaluations (gen-vals (free-vars f)))
  57.          (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations)))
  58.     (ormap false? results)))
  59.  
  60. (define (nff? f)
  61.   (cond [(lit? f) true]
  62.         [(neg? f) false]
  63.         [(conj? f) (and (nff? (conj-left f))
  64.                         (nff? (conj-right f)))]
  65.         [(disj? f) (and (nff? (disj-left f))
  66.                         (nff? (disj-right f)))]
  67.         [else (error "Zła formuła -- NFF?" f)]))
  68.  
  69. (define (convert-to-nnf f)
  70.   (cond [(lit? f) f]
  71.         [(neg? f) (convert-negation (neg-subf f))]
  72.         [(conj? f) (conj (convert-to-nnf (conj-left f))
  73.                               (convert-to-nnf (conj-right f)))]
  74.         [(disj? f) (disj (convert-to-nnf (disj-left f))
  75.                               (convert-to-nnf (disj-right f)))]
  76.         [else (error "Zła formuła -- CONVERT" f)]))
  77.  
  78. (define (convert-negation f)
  79.   (cond [(lit? f)
  80.          (if (var? f)
  81.              (neg f)
  82.              (neg-subf f))]
  83.         [(neg? f) (convert-to-nnf (neg-subf f))]
  84.         [(conj? f) (disj (convert-negation (conj-left f))
  85.                               (convert-negation (conj-right f)))]
  86.         [(disj? f) (conj (convert-negation (disj-left f))
  87.                               (convert-negation (disj-right f)))]
  88.         [else (error "Zła formuła -- CONVERT-NEGATION" f)]))
  89.  
  90. (define (clause? x)
  91.   (and (list? x)
  92.        (andmap lit? x)))
  93.  
  94. (define (clause-empty? x)
  95.   (and (clause? x)
  96.        (null? x)))
  97.  
  98. (define (cnf? x)
  99.   (and (list? x)
  100.        (andmap clause? x)))
  101.  
  102. (define (flatmap proc seq)
  103.   (foldl append null (map proc seq)))
  104.  
  105. (define (convert-to-cnf f)
  106.   (define (convert f)
  107.     (cond [(lit? f) (list (list f))]
  108.           [(conj? f) (append (convert-to-cnf (conj-left f))
  109.                              (convert-to-cnf (conj-right f)))]
  110.           [(disj? f)
  111.            (let ((clause-left (convert-to-cnf (disj-left f)))
  112.                  (clause-right (convert-to-cnf (disj-right f))))
  113.              (flatmap (λ (clause)
  114.                         (map (λ (clause2)
  115.                                (append clause2 clause)) clause-left))
  116.                       clause-right))]))
  117.   (convert (convert-to-nnf f)))
  118.  
  119. (define (falsifiable-clause? clause)
  120.   (cond [(clause-empty? clause) true]
  121.         [(lit? (findf (λ (l) (equal?
  122.                               l
  123.                               (convert-to-nnf (neg (car clause)))))
  124.                               clause)) false]
  125.         [else (falsifiable-clause? (cdr clause))]))
  126.  
  127. (define (falsifiable-cnf? f)
  128.   (define (neg-value lit)
  129.     (if (var? lit)
  130.         (list lit false)
  131.         (list (neg-subf lit) true)))
  132.   (ormap (λ (clause) (if (falsifiable-clause? clause)
  133.                          (map neg-value clause)
  134.                         false))
  135.          (convert-to-cnf f)))
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement