1 files changed, 0 insertions, 140 deletions
diff --git a/Semestr 2/racket/lista5/solution.rkt b/Semestr 2/racket/lista5/solution.rkt
deleted file mode 100644
index 67964d8..0000000
--- a/Semestr 2/racket/lista5/solution.rkt
+++ /dev/null
@@ -1,140 +0,0 @@
-#lang racket
-
-(provide falsifiable-cnf?)
-(require "props.rkt")
-
-(define (prop? f)
-  (or (var? f)
-      (and (neg? f)
-           (prop? (neg-subf f)))
-      (and (disj? f)
-           (prop? (disj-left f))
-           (prop? (disj-right f)))
-      (and (conj? f)
-           (prop? (conj-left f))
-           (prop? (conj-right f)))))
-
-(define (lit? t)
-  (or (var? t)
-      (and (neg? t)
-           (var? (neg-subf t)))))
-
-(define (lit-var f)
-  (cond [(var? f) f]
-        [(neg? f) (neg-subf f)]
-        [else (error "Złe dane ze znacznikiem -- LIT-VAR" f)]))
-      
-(define (free-vars f)
-  (cond [(null? f) null]
-        [(var? f) (list f)]
-        [(neg? f) (free-vars (neg-subf f))]
-        [(conj? f) (append (free-vars (conj-left f))
-                           (free-vars (conj-right f)))]
-        [(disj? f) (append (free-vars (disj-left f))
-                           (free-vars (disj-right f)))]
-        [else (error "Zła formula -- FREE-VARS" f)]))
-
-(define (gen-vals xs)
-  (if (null? xs)
-      (list null)
-      (let*
-          ((vss (gen-vals (cdr xs)))
-           (x (car xs))
-           (vst (map (λ (vs) (cons (list x true) vs)) vss))
-           (vsf (map (λ (vs) (cons (list x false) vs)) vss)))
-        (append vst vsf))))
-
-(define (eval-formula f evaluation)
-  (cond [(var? f)
-         (let ((val (assoc f evaluation)))
-           (if (not val)
-               (error "Zmienna wolna nie wystepuje w wartościowaniu -- EVAL-FORMULA" f evaluation)
-               (cadr val)))]
-        [(neg? f) (not (eval-formula (neg-subf f) evaluation))]
-        [(disj? f) (or (eval-formula (disj-left f) evaluation)
-                       (eval-formula (disj-right f) evaluation))]
-        [(conj? f) (and (eval-formula (conj-left f) evaluation)
-                        (eval-formula (conj-right f) evaluation))]
-        [else (error "Zła formuła -- EVAL-FORMULA" f evaluation)]))
-
-(define (falsifiable-eval? f)
-  (let* ((evaluations (gen-vals (free-vars f)))
-         (results (map (λ (evaluation) (eval-formula f evaluation)) evaluations)))
-    (ormap false? results)))
-
-(define (nff? f)
-  (cond [(lit? f) true]
-        [(neg? f) false]
-        [(conj? f) (and (nff? (conj-left f))
-                        (nff? (conj-right f)))]
-        [(disj? f) (and (nff? (disj-left f))
-                        (nff? (disj-right f)))]
-        [else (error "Zła formuła -- NFF?" f)]))
-
-(define (convert-to-nnf f)
-  (cond [(lit? f) f]
-        [(neg? f) (convert-negation (neg-subf f))]
-        [(conj? f) (conj (convert-to-nnf (conj-left f))
-                              (convert-to-nnf (conj-right f)))]
-        [(disj? f) (disj (convert-to-nnf (disj-left f))
-                              (convert-to-nnf (disj-right f)))]
-        [else (error "Zła formuła -- CONVERT" f)]))
-
-(define (convert-negation f)
-  (cond [(lit? f)
-         (if (var? f)
-             (neg f)
-             (neg-subf f))]
-        [(neg? f) (convert-to-nnf (neg-subf f))]
-        [(conj? f) (disj (convert-negation (conj-left f))
-                              (convert-negation (conj-right f)))]
-        [(disj? f) (conj (convert-negation (disj-left f))
-                              (convert-negation (disj-right f)))]
-        [else (error "Zła formuła -- CONVERT-NEGATION" f)]))
-
-(define (clause? x)
-  (and (list? x)
-       (andmap lit? x)))
-
-(define (clause-empty? x)
-  (and (clause? x)
-       (null? x)))
-
-(define (cnf? x)
-  (and (list? x)
-       (andmap clause? x)))
-
-(define (flatmap proc seq)
-  (foldl append null (map proc seq)))
-
-(define (convert-to-cnf f)
-  (define (convert f)
-    (cond [(lit? f) (list (list f))]
-          [(conj? f) (append (convert-to-cnf (conj-left f))
-                             (convert-to-cnf (conj-right f)))]
-          [(disj? f)
-           (let ((clause-left (convert-to-cnf (disj-left f)))
-                 (clause-right (convert-to-cnf (disj-right f))))
-             (flatmap (λ (clause)
-                        (map (λ (clause2)
-                               (append clause2 clause)) clause-left))
-                      clause-right))]))
-  (map (lambda (clause) (remove-duplicates clause)) (convert (convert-to-nnf f))))
-
-(define (falsifiable-clause? clause)
-  (cond [(clause-empty? clause) true]
-        [(lit? (findf (λ (l) (equal?
-                              l
-                              (convert-to-nnf (neg (car clause)))))
-                              clause)) false]
-        [else (falsifiable-clause? (cdr clause))]))
-
-(define (falsifiable-cnf? f)
-  (define (neg-value lit)
-    (if (var? lit)
-        (list lit false)
-        (list (neg-subf lit) true)))
-  (ormap (λ (clause) (if (falsifiable-clause? clause)
-                         (map neg-value clause)
-                         false))
-         (convert-to-cnf f)))
-\ No newline at end of file