tp logique scheme

#lang racket

; 1 Représentation des propositions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define F '(<-> (^ a c) (v (! b) (-> c (^ B T)))))

; Q1
(define F1 '(<-> (^ a b) (! (v a b))))
(define F2 '(v (! (^ a (! b))) (! (-> a b))))
(define F3 '(^ (! (-> a (v a b))) (! (! (^ a (v b (! c)))))))

(define F5 '())

(define FX '(v a b)
  )

(define F4 '(^
             (v (v
                 (! a)
                 b)
                d)
             (^
              (v
               (! d)
               c)
              (^
               (v c a)
               (^
                (v
                 (! c)
                 b)
                (^
                 (v
                  (! c)
                  (! b))
                 (v
                  (! b)
                  d)
                 )
                )
               )
              )
             )
  )


; Q2
(define (neg? f) (eq? f '!))
(define (and? f) (eq? f '^))
(define (or? f) (eq? f 'v))
(define (imp? f) (eq? f '->))
(define (equ? f) (eq? f '<->))
(define (top? f) (eq? f 'T))
(define (bot? f) (eq? f 'B))
(define (symbLog? f) (or (top? f) (bot? f) (and? f) (or? f) (neg? f) (imp? f) (equ? f)))
(define (symbProp? f) (and (symbol? f) (not (symbLog? f))))
(define (atomicFbf? f) (or (symbProp? f) (top? f) (bot? f)))
(define (conBin? f) (or (and? f) (or? f) (imp? f) (equ? f)))

; Q2
(define (fbf? f)
  (cond ((atomicFbf? f) #t)
        ((list? f) (cond ((and (= (length f) 2) (neg? (car f))) (fbf? (cadr f)))
                         ((and (= (length f) 3) (conBin? (car f))) (and (fbf? (cadr f)) (fbf? (caddr f))))
                         (else #f)))
        (else #f)))

(define (fbf2? f)
  (cond ((atomicFbf? f) (begin (display " case1 : " ) (display f) #t))
        ((list? f) (cond ((and (= (length f) 2) (neg? (car f)))  (begin (display " case2.1 : f = ") (display f) (display " ; car f = " ) (display (car f)) (display " cdr f = ") (display (cdr f)) (fbf2? (cadr f))))
                         ((and (= (length f) 3) (conBin? (car f))) (begin (display " case2.2 : f = " ) (display f) (display " ; car f = " ) (display (car f)) (display " cadr f = ") (display (cadr f)) (display " caddr f = ") (display (caddr f)) (and (fbf2? (cadr f)) (fbf2? (caddr f)))))
                         (else (begin (display " case2.1 : f = " ) (display f) #f))))
        (else (and (display " case3 : ") #f)))
  )

(define (fbf3? f)
  (cond ((atomicFbf? f) (begin (display 't1) #t))
        ((list? f) (cond ((and (= (length f) 2) (neg? (car f)))  (begin (display 't2) (fbf3? (cadr f))))
                         ((and (= (length f) 3) (conBin? (car f))) (begin (display 't3) (and (fbf3? (cadr f)) (fbf3? (caddr f)))))
                         (else (begin (display 't4) #f))))
        (else (begin (display 't5) #f))
        )
  )

(define (fbfp p)
  (define  (X p1)
    (cond
      ((eq? p1 '()) #t)
      ((not (eq? '() p1)) (and (fbfp (car p1))))
      )
    )
  (X (cdr p))
  )


; 2 Syntaxe des propositions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(display " ")
(define (conRac f) (car f))
(define (fils f) (cadr f))
(define (filsG f) (cadr f))
(define (filsD f) (caddr f))
(define (negFbf? f) (and (not (atomicFbf? f)) (neg? (conRac f))))

; Q3
(define (nbc? f)
  (cond ((atomicFbf? f) 0)
        ((negFbf? f) (+ 1 (nbc? (fils f))))
        (#t (+ 1 (nbc? (filsG f)) (nbc? (filsD f))))))


; Q4
(define (prof? f)
  (cond ((atomicFbf? f) 0)
        ((negFbf? f) (+ 1 (prof? (fils f))))
        (#t (max (+ 1 (prof? (filsG f))) (+ 1 (prof? (filsD f)))))
        )
  )

; Q5

(define (ensSP? f)
  (cond
    [(atomicFbf? f) (set-add '() f)]
    [(negFbf? f) (set-union (ensSP? (cadr f)))]
    [#t (set-union (ensSP? (cadr f)) (ensSP? (caddr f)))]
    )
  )

; Q6
(define (affiche fbf)
  (cond
    [(atomicFbf? fbf) (display fbf)]
    [(negFbf? fbf) (begin (display "(") (display "¬") (affiche (fils fbf)) (display ")"))]
    [#t
     (begin (display "(") (affiche (filsG fbf)) (display " ") (display (car fbf)) (display " ") (affiche (filsD fbf)) (display ")"))]
    )
  )


(define (affiche2 fbf)
  (begin (display "(")
         (display
          (cond
            [(atomicFbf? fbf) (symbol->string fbf)]
            [(negFbf? fbf) (string-append " ! " (affiche (fils fbf)))]
            [#t (string-append (affiche (filsG fbf)) (string-append " " (string-append (car fbf) (string-append " " (affiche (filsD fbf))))))]
            )
          )
         (display ")")
         )
  )

; Q7
(define I1(cons (cons 'a 1) (cons (cons 'c 1) (cons (cons 'b 0) null))))
(define I2(cons (cons 'a 0) (cons (cons 'c 0) (cons (cons 'b 0) null))))
(define I3(cons (cons 'a 1) (cons (cons 'c 1) (cons (cons 'b 1) null))))

; Q8
(define (intSymb symb itp)
  (cond
    [(eq? symb (caar itp)) (cdar itp)]
    [#t (intSymb symb (cdr itp))]
    )
  )

; Q9
(define (intNeg b)
  (if (eq? b 0) 1 0)
  )
(define (intAnd b1 b2)
  (if (and (eq? b1 1) (eq? b2 1)) 1 0)
  )
(define (intOr b1 b2)
  (if (or (eq? b1 1) (eq? b2 1)) 1 0)
  )
(define (intImp b1 b2)
  (if (eq? b1 0) 1 b2)
  )
(define (intEqu b1 b2)
  (if (eq? (if (eq? b1 0) 1 b2) (if (eq? b2 0) 1 b1)) 1 0)
  )
(define intTop 1)
(define intBot 0)

; Q10
(define (valV f i)
  (cond [(symbProp? f) (intSymb f i)]
        [(top? f) intTop]
        [(bot? f) intBot]
        [(negFbf? f) (intNeg (valV (fils f) i))]
        [(and? (conRac f)) (intAnd (valV (filsG f) i) (valV (filsD f) i))]
        [(or? (conRac f)) (intOr (valV (filsG f) i) (valV (filsD f) i))]
        [(imp? (conRac f)) (intImp (valV (filsG f) i) (valV (filsD f) i))]
        [(equ? (conRac f)) (intEqu (valV (filsG f) i) (valV (filsD f) i))]
        [#t 0]
        )
  )

; Q11
(define (modele? i fbf)
  (eq? (valV fbf i) 1)
  )

; Q12
(define ensISP
  (list
   (list (cons 'p 0) (cons 'q 0))
   (list (cons 'p 0) (cons 'q 1))
   (list (cons 'p 1) (cons 'q 0))
   (list (cons 'p 1) (cons 'q 1))
   )
  )

; Q13
(define (ensInt ESP)
  (cond ((set-empty? ESP) (list null))
        (else (let ((ensIntCdr(ensInt (cdr ESP))))
                (set-union
                 (map [lambda (i) (cons (cons (car ESP) 0) i)] ensIntCdr)
                 (map [lambda (i) (cons (cons (car ESP) 1) i)] ensIntCdr)
                 )
                )
              )
        )
  )

(define (ensInt2 ESP)
  (cond ((null? ESP) '(()))
        (else (let ((I (ensInt (cdr ESP))))
                (append
                 (map [lambda (i) (set-add i (cons (car ESP) 0))] I)
                 (map [lambda (i) (set-add i (cons (car ESP) 1))] I)
                 )
                )
              )
        )
  )

; Q14
(define (satisfiable? fbf)
  (ormap (lambda (i) (modele? i fbf)) (ensInt (ensSP? fbf)))
  )

; Q15
(define (valide? fbf)
  (andmap (lambda (i) (modele? i fbf)) (ensInt (ensSP? fbf)))
  )

; Q16
(define (insatisfiable? fbf)
  (not (andmap (lambda (i) (modele? i fbf)) (ensInt (ensSP? fbf)))
       )
  )

; Q17
(define (test2FbfAvecInterpretations fbf1 fbf2 i)
  (cond ((null? i) #t)
        ((eq? (valV fbf1 (car i)) (valV fbf2 (car i))) (test2FbfAvecInterpretations fbf1 fbf2 (cdr i)))
        [else #f]
        )
  )

(define (equivalent1? f1 f2)
  (test2FbfAvecInterpretations f1 f2 (ensInt (set-union (ensSP? f1) (ensSP? f2))))
  )

(define (equivalent1v2? f1 f2)
  (andmap (lambda (i)
            (= (valV f1 i) (valV f2 i)))
          (ensInt (set-union (ensSP? f1) (ensSP? f2)))
          )
  )

(define (equivalent2? f1 f2)
  (valide? (list '<-> f1 f2))
  )

; Q18
(define (consequence2? f g)
  (andmap (lambda (i)
            (if (and (eq? (valV f i) 1) (= (valV g i) 0)) #f #t)
            )
          (ensInt (set-union (ensSP? f) (ensSP? g)))
          )
  )

(define (consequence2v2? f g)
  (insatisfiable? (list '^ f (list '! g)))
  )

(define (consequence2v3? f g)
  (valide? (list '-> f g))
  )

; Q19
(define (ensSPallFbf eFbf)
  (if (set-empty? eFbf) '()
      (set-union (ensSP? (car eFbf))
                 (ensSPallFbf (cdr eFbf))
                 )
      )
  )

; Q20
(define (modeleCommun? i ensFBF)
  (cond [(set-empty? ensFBF)]
        [(modele? i (car ensFBF)) (modeleCommun? i (cdr ensFBF))]
        [else #f]
        )
  )
(define (modeleCommunv2? i ensFBF)
  (andmap (lambda (fbf) (modele? i fbf)) ensFBF)
  )

; Q21
(define (contradictoire? ensFBF)
  (not (ormap (lambda (i) (modeleCommun? i ensFBF)) (ensInt (ensSPallFbf ensFBF))
          )
       )
  )
(define (contradictoirev2? ensFBF)
  (andmap (lambda (i) (not (modeleCommun? i ensFBF))) (ensInt (ensSPallFbf ensFBF))
          )
  )

; Q22
(define (consequence? ensFBF f)
  (let ((ensF (set-union ensFBF f)))
    (ormap (lambda (i) (modeleCommun? i ensF)) (ensInt (set-union (ensSPallFbf ensFBF) (ensSP? f))))
    )
  )

; Q23