==== 15/09/16  es. 2.

L ::= [] | N::L

Problema: f(L) deve ordinare L

f([]) = []
f(N::L) = i(f(L),N)

Problema: data una lista ordinata L e un numero N, aggiungerlo alla lista
Soluzione: i(L,N)

i([],N) = N::[]
i(M::L,N) =
 if N <= M then
  N::M::L
 else
  M::i(L,N)

==== 15/09/16  es. 3.
Calcolare il numero di connettivi ternari degeneri

Es:  *(A,B,C) = A /\ B

quanti connettivi binari esistono? 16
i ternari degeneri sono 3 * 3 * 16

==== 15/09/16  es. 5.
Teorema di correttezza per la logica proposizionale classica:
per ogni Gamma e per ogni F, se Gamma |- F allora Gamma |= F
dove posso usare anche la RAA

==== 15/09/16  es. 6.
not(not(A)) == A
A \/ -A == Top

==== 15/09/16  es. 7.
F ::= A | B | ... | bot | top | F /\ F

Teorema: se |- F[bot/A] allora per ogni G, |- F[G/A]

Dimostrazione: per induzione strutturale su F

Caso A:
  dimostro che  |- A[bot/A] allora per ogni G, |- A[G/A]
  ovvero che    |- bot      allora  per ogni G, |- G
  la premessa è falsa quindi l'enunciato è vero

Caso B:
  dimostro che  |- B[bot/A] allora per ogni G, |- B[G/A]
  ovvero che    |- B        allora per ogni G, |- B
  ovvio

...

Caso bot:
  dimostro che  |- bot[bot/A] allora per ogni G, |- bot[G/A]
  ovvero che  |- bot allora per ogni G, |- bot
  la premessa è falsa quindi l'enunciato è vero

Caso top:
  dimostro che  |- top[bot/A] allora per ogni G, |- top[G/A]
  ovvero che  |- top allora per ogni G, |- top
  la conclusione è vera quindi l'enunciato è vero

Caso F1 /\ F2:
  per ipotesi induttiva  se |- F1[bot/A] allora per ogni G, |- F1[G/A]
  per ipotesi induttiva  se |- F2[bot/A] allora per ogni G, |- F2[G/A]
  dimostro se |- (F1 /\ F2)[bot/A] allora per ogni G, |- (F1 /\ F2)[G/A]
  ovvero che se |- F1[bot/A] /\ F2[bot/A]
  allora per ogni G, |- F1[G/A] /\ F2[G/A]
  assumo che |- F1[bot/A] /\ F2[bot/A]
  fisso H e dimostro  |- F1[H/A] /\ F2[H/A]

      ..                      ..
     ipotesi                 ipotesi
      ..                      ..
  F1[bot/A] /\ F2[bot/A]   F1[bot/A] /\ F2[bot/A] 
  ============ /\e1        ============ /\e2
    F1[bot/A]               F2[bot/A]
       ..                     ..
       IH                     IH
       ..                     ..
    F1[H/A]                  F2[H/A]
  ==================================== /\i
            F1[H/A] /\ F2[H/A]


==== 02/02/17  es. 2.
L ::= [] | N::L

Problema: f(L) tiene solo i duplicati e una volta sola

f([]) = []
f(N::L) = if in(N,L) && not(in(N,f(L))) then N::f(L) else f(L)

Problema: data una lista e un numero, restitiuire true se il numero occorre nella lista
Soluzione: in(N,L)

in(N,[]) = false
in(N,M::L) = (N=M) || in(N,L)


==== 02/02/17  es. 7.
F ::= top | A | F /\ F

f(top) = top
f(A) = A
f(F1 /\ F2) = if f(F1) = f(F2) then f(F1) else f(F1) /\ f(F2)

Teorema: per ogni F, se |= F allora f(F) = top
Dimostrazione: per induzione strutturale su F

Caso top:
  dimostro se |= top allora f(top) = top
  ovvero che  se |= top allora top = top
  ovvio

Caso A:
  dimostro se |= A allora f(A) = top
  ovvio perchè la premessa è falsa

Caso F1 /\ F2:
  ipotesi induttiva  se |= F1 allora f(F1) = top
  ipotesi induttiva  se |= F2 allora f(F2) = top
  dimostro se |= F1 /\ F2 allora f(F1 /\ F2) = top
  ovvero che se  |= F1 /\ F2 allora if f(F1) = f(F2) then f(F1) else f(F1) /\ f(F2) = top
  suppongo |= F1 /\ F2
  quindi |= F1 e |= F2 perchè in tutti i mondi il minimo fa 1 ...
  quindi, usando le ipotesi induttive, f(F1) = top e f(F2) = top
  dimostro if f(F1) = f(F2) then f(F1) else f(F1) /\ f(F2) = top
  ovvero   if top = top then top else top /\ top = top
  ovvero   top = top
  ovvio

Teorema: per ogni F, se f(F) = top allora |= F 
Dimostrazione: per induzione strutturale su F

Caso top:
  dimostro che se f(top) = top allora |= top
  ovvio perchè la conclusione è vera

Caso A:
  dimostro che se f(A) = top allora |= A
  ovvero che        A = top  allora |= A
  ovvio perchè la premessa è falsa

Caso F1 /\ F2:
  ipotesi induttiva che se f(F1) = top allora |= F1
  ipotesi induttiva che se f(F2) = top allora |= F2
  dimostro che se f(F1 /\ F2) = top allora |= F1 /\ F2
  ovvero che se
   if f(F1) = f(F2) then f(F1) else f(F1) /\ f(F2) = top
  allora |= F1 /\ F2
  assumo if f(F1) = f(F2) then f(F1) else f(F1) /\ f(F2) = top
  e dimostro |= F1 /\ F2
  per casi su  f(F1) = f(F2)  oppure not(f(F1) = f(F2)):
  caso f(F1) = f(F2):
    so if true then f(F1) else f(F1) /\ f(F2) = top
    ovvero f(F1) = top
    per ipotesi induttiva |= F1
    inoltre f(F2) = top anche lei perchè f(F1) = f(F2)
    quindi per l'altra ipotesi induttiva |= F2
    e quindi |= F1 /\ F2 perchè il minimo ...
  caso not(f(F1) = f(F2)):
    so if false then f(F1) else f(F1) /\ f(F2) = top
    ovvero f(F1) /\ f(F2) = top
    assurdo
    ovvio

==== 12/06/17  es. 2.
F ::= A | B | .... | bot | F /\ F

Problema: sub(F,G) ritorna true sse G è sottoformula di F

sub(A,G) = (A = G)
...
sub(bot,G) = (bot = G)
sub(F1 /\ F2, G) = sub(F1,G) || sub(F2,G) || (F1 /\ F2 = G)

==== 12/06/17  es. 7.
Teorema: se G == bot e se sub(F,G) = true allora F == bot
Dimostrazione: per induzione strutturale su F

Caso A:
  dimostro che se G == bot e sub(A,G) = true  allora A == bot
  ovvero che   se G == bot e (A=G) = true  allora A == bot
  assumo G == bot e che (A=G) = true
  quindi A = G
  dimostro A == bot ovvero G == bot
  ovvio per ipotesi

...

caso bot:
  dimostro che se G == bot e sub(bot,G) = true  allora bot == bot
  ovvio perchè la conclusione è vera

caso F1 /\ F2:
  ipotesi induttiva che se G == bot e sub(F1,G) = true  allora F1 == bot
  ipotesi induttiva che se G == bot e sub(F2,G) = true  allora F2 == bot
  dimostro che se G == bot e sub(F1/\F2,G) = true  allora F1/\F2 == bot
  ovvero che se G == bot e sub(F1,G) || sub(F2,G) || (F1/\F2=G) = true  allora F1/\F2 == bot
  assumo G == bot e  sub(F1,G) || sub(F2,G) || (F1/\F2=G) = true
  quindi sub(F1,G) = true o sub(F2,G) = true o F1/\F2 = G
  procedo per casi:
  caso sub(F1,G) = true:
    per ipotesi induttiva F1 == bot
    e quindi F1/\F2 == bot
  caso sub(F2,G) = true:
    per ipotesi induttiva F2 == bot
    e quindi F1/\F2 == bot
  caso F1/\F2 = G:
    per ipotesi G == bot
    e quindi F1/\F2 == bot