---
tags: mp, WCh
---

# Lista 5

Formuły:

(define (var? t)
  (symbol? t))

(define (neg? t)
  (and (list? t)
       (= 2 (length t))
       (eq? 'neg (car t))))

(define (conj? t)
  (and (list? t)
       (= 3 (length t))
       (eq? 'conj (car t))))

(define (disj? t)
  (and (list? t)
       (= 3 (length t))
       (eq? 'disj (car t))))

(define (prop? f)
  (or (var? f)
      (and (neg? f)
           (prop? (neg-subf f)))
      (and (disj? f)
           (prop? (disj-left f))
           (prop? (disj-rght f)))
      (and (conj? f)
           (prop? (conj-left f))
           (prop? (conj-rght f)))))

## Ćwiczenie 1

(define (make-neg f)
    (list 'neg f))
    
(define (make-conj l r)
    (list 'conj l r))
    
(define (make-disj l r)
    (list 'disj l r))
    
(define (neg-subf f)
    (second f))

(define (conj-left f)
    (second f))
    
(define (conj-rght f)
    (third f))
    
(define (disj-left f)
    (second f))
    
(define (disj-rght f)
    (third f))
    
(define tauthology (make-disj 'p (make-neg 'p)))
(define some-formula (make-conj 'p 'q))

## Ćwiczenie 2

Indukcja po podformułach.

(define (prop? f)
    (or (var? f)
        (and (neg? f)
             (prop? (neg-subf f)))
        (and (disj? f)
             (prop? (disj-left f))
             (prop? (disj-rght f)))
        (and (conj? f)
             (prop? (conj-left f))
             (prop? (conj-rght f)))))

Zasada indukcji. Dla dowolnej własności P, jeśli:

* dla każdego symbolu x zachodzi P(x),
* dla dowolnej formuły f, jeśli zachodzi P(f), to zachodzi P((neg f)) i
* dla dowolnych formuł f1, f2, jeśli zachodzi P(f1) i P(f2), to zachodzi również P((conj f1 f2)) i P((disj f1 f2))

to dla dowolnej formuły f, jeśli zachodzi (prop? f), to zachodzi P(f).

## Ćwiczenie 3

(define (free-vars f)
    (define (go f)
        (cond ((var? f)
               (list f))
              ((neg? f)
               (go (neg-subf f)))
              ((disj? f)
               (append (go (disj-left f)) 
                       (go (disj-rght f))))
              ((conj? f)
               (append (go (conj-left f)) 
                       (go (conj-rght f))))))
    (remove-duplicates (go f)))

(free-vars tauthology)
(free-vars some-formula)

## Ćwiczenie 4

(define (gen-vals xs)
  (if (null? xs)
      (list null)
      (let*
          ((vss  (gen-vals (cdr xs)))
           (x    (car xs))
           (vst  (map (lambda (vs) (cons (list x true)  vs)) vss))
           (vsf  (map (lambda (vs) (cons (list x false) vs)) vss)))
        (append vst vsf))))

(define (eval-formula f v)
    (cond
        ((var? f) (second (assoc f v)))
        ((neg? f) (not (eval-formula (neg-subf f) v)))
        ((conj? f) (and
            (eval-formula (conj-left f) v)
            (eval-formula (conj-rght f) v)))
        ((disj? f) (or
            (eval-formula (disj-left f) v)
            (eval-formula (disj-rght f) v)))
    ))

; (define second cadr)
; (define (cadr x) (car (cdr x)))
; (define head car)
; (define tail cdr)

(define (falsifiable-eval? f)
    (define (is-false v)
        (not (eval-formula f v)))
    (let* [
        (vars (free-vars f))
        (all-vals (gen-vals vars))
        (false-vals (filter is-false all-vals))
        ]
        (if (= (length false-vals) 0)
            false
            (first false-vals))))

(define (falsifiable-eval2? f)
    (define (is-false v)
        (if (not (eval-formula f v))
            v
            false))
    (let* [
        (vars (free-vars f))
        (all-vals (gen-vals vars))
        ]
        (ormap is-false all-vals)))

(define (falsifiable-eval3? f)
    (define (is-true v)
        (eval-formula f v))
    (let* [
        (vars (free-vars f))
        (all-vals (gen-vals vars))
        (false-vals (dropf all-vals is-true))
        ]
        (if (= (length false-vals) 0)
            false
            (first false-vals))))

(falsifiable-eval? some-formula)

## Ćwiczenie 5

(define (nnf? f)
    (or (var? f)
        (and (neg? f)
             (var? (neg-subf f)))
        (and (disj? f)
             (nnf? (disj-left f))
             (nnf? (disj-rght f)))
        (and (conj? f)
             (nnf? (conj-left f))
             (nnf? (conj-rght f)))))

;; (make-literal false p) - zanegowane p, wpp niezanegowane
(define (make-literal b p)
    (list 'literal b p))

(define (literal? f)
    (and (= 3 (length f))
         (eq? 'literal (first f))
         (boolean? (second f))
         (var? (third f))))

(define (literal-positive? f)
    (second f))

(define (literal-var f)
    (third f))

(define (nnf? f)
    (or (var? f)
        (literal? f)
        (and (disj? f)
             (nnf? (disj-left f))
             (nnf? (disj-rght f)))
        (and (conj? f)
             (nnf? (conj-left f))
             (nnf? (conj-rght f)))))

(define (free-vars-nnf f)
    (define (go f)
        (cond ((var? f)
               (list f))
              ((literal? f)
               (list (literal-var f)))
              ((neg? f)
               (go (neg-subf f)))
              ((disj? f)
               (append (go (disj-left f)) 
                       (go (disj-rght f))))
              ((conj? f)
               (append (go (conj-left f)) 
                       (go (conj-rght f))))))
    (remove-duplicates (go f)))
    
(define (eval-formula-nnf f v)
    (cond
        ((var? f) (second (assoc f v)))
        ((literal? f)
            (let ((var-val (second (assoc (literal-var f)) v)))
                 (if (literal-positive? f)
                     var-val
                     (not var-val))))
        ((neg? f) (not (eval-formula-nnf (neg-subf f) v)))
        ((conj? f) (and
            (eval-formula-nnf (conj-left f) v)
            (eval-formula-nnf (conj-rght f) v)))
        ((disj? f) (or
            (eval-formula-nnf (disj-left f) v)
            (eval-formula-nnf (disj-rght f) v)))
    ))

(define definitely-false (make-conj 'p (make-literal false 'p)))
(define tauthology-nnf (make-disj 'p (make-literal false 'p)))

## Ćwiczenie 6

; zbiór zadań z logiki s. 35 (rysunek 5.)
(define (convert-to-nnf f)
    (define (T f)
        (cond
            [(var? f) (make-literal true f)]
            [(neg? f) (F (neg-subf f))]
            [(conj? f) (make-conj
                (T (conj-left f))
                (T (conj-rght f)))]
            [(disj? f) (make-disj
                (T (disj-left f))
                (T (disj-rght f)))]
        )
    )
    (define (F f)
        (cond
            [(var? f) (make-literal false f)]
            [(neg? f) (T (neg-subf f))]
            [(conj? f) (make-disj
                (F (conj-left f))
                (F (conj-rght f)))]
            [(disj? f) (make-conj
                (F (disj-left f))
                (F (disj-rght f)))]
        )
    )
    (T f)
)

(define in-nnf (convert-to-nnf (make-neg (make-disj 'p 'q))))
(nnf? in-nnf)

## Ćwiczenie 7

Zestaw równoważności:
(neg-subf (make-neg p)) = p

(conj-left (make-conj p q)) = p
(conj-rght (make-conj p q)) = q

(disj-left (make-disj p q)) = p
(disj-rght (make-disj p q)) = q

P(f) ≡ (nnf? (convert-to-nnf f)) = true

Zasada indukcji. Dla dowolnej własności P, jeśli:

dla każdego symbolu x zachodzi P(x),
dla dowolnej formuły f, jeśli zachodzi P(f), to zachodzi P((neg f)) i
dla dowolnych formuł f1, f2, jeśli zachodzi P(f1) i P(f2), to zachodzi również P((conj f1 f2)) i P((disj f1 f2))

to dla dowolnej formuły f, jeśli zachodzi (prop? f), to zachodzi P(f).

(define (T f)
    (cond
        [(var? f) (make-literal true f)]
        [(neg? f) (F (neg-subf f))]
        [(conj? f) (make-conj
            (T (conj-left f))
            (T (conj-rght f)))]
        [(disj? f) (make-disj
            (T (disj-left f))
            (T (disj-rght f)))]
    )
)
    
(define (F f)
    (cond
        [(var? f) (make-literal false f)]
        [(neg? f) (T (neg-subf f))]
        [(conj? f) (make-disj
            (F (conj-left f))
            (F (conj-rght f)))]
        [(disj? f) (make-conj
            (F (disj-left f))
            (F (disj-rght f)))]
    )
)

;; Silniejsza własność P
P(f) ≡ (nnf? (T f)) i (nnf? (F f))

Weźmy dowolny symbol x. Pokażmy, że P(x):
L - lewa strona
L ≡ (nnf? (T x)) ≡ (nnf? (make-literal true x)) ≡ true
P ≡ (nnf? (F x)) ≡ (nnf? (make-literal false x)) ≡ true

Weźmy dowolną formułę f i załóżmy, że P(f). Pokażmy, że P(not f):
L ≡ (nnf? (T (make-neg f))) ≡ (nnf? (F f)) ≡ true
P ≡ (nnf? (F (make-neg f))) ≡ (nnf? (T f)) ≡ true

Weźmy dowolne formuły f1, f2 i załóżmy, że P(f1) i P(f2). Pokażmy, że:
a) P(conj f1 f2)
L ≡ (nnf? (T (make-conj f1 f2))) ≡ (nnf? (make-conj (T f1) (T f2))
≡ (and (nnf? (T f1)) (nnf? (T f2))) ≡ true
Dla prawej strony tak samo

b) P(disj f1 f2)
Analogicznie

Zatem na mocy zasady o indukcji, P(f) zachodzi dla dowolnej formuły f (czyli (T f) zamienia dowolną formułę na nnf)

Skoro (convert-to-nnf f) ≡ (T f), to udowodniliśmy, że procedura convert-to-nnf zamienia dowolną formułę f na nnf.

## Ćwiczenie 8

zabrakło nam na to czasu