Esercizio 1

Dire quali delle seguenti sentenze è valida, giustificando la risposta.

(a) (\exist x  x=x) => (\forall y \exist z y=z)
  
    RISPOSTA: valida. La premessa dell'implicazione è vera in ogni modello
    con un oggetto, che è sempre il caso in FOL. Poiché c'è un oggetto,
    allora per ogni y possiamo trovare una z (in particolare l'oggetto
    riferito da y) che è lo stesso di y.

(b) \forall x  P(x) OR ¬P(x)

    RISPOSTA: valida, infatti per ogni valore fissato per x, 
    P(x) OR ¬P(x) è una sentenza valida nella logica proposizionale.

(c) \forall x S(x) OR (x=x)

    RISPOSTA: valida. Per ogni x, x=x è vera, e quindi la disgiunzione
    è vera.


Esercizio 2

Si consideri una base di conoscenza con le seguenti clausole:
    P(f(x)) => P(x)
    Q(x) => P(f(x))
    P(a)
    Q(b)
dove x è una variabile ed a e b sono costanti. Indichiamo con FC l'algoritmo
di forward chaining e con BC l'algoritmo di backward chaining, che
seleziona le clausole nell'ordine di occorrenza dato.

(a) dire se FC inferisce il letterale Q(a) e spiegare perché.

    RISPOSTA: No. Q(a) non è conseguenza logica della base di conoscenza.

(b) dire se FC inferisce il letterale P(b) e spiegare perché.

    RISPOSTA: Si, attraverso la generazione di P(f(b)).

(c) se FC fallisce ad inferire un dato letterale, è vero concludere
    che tale letterale non è conseguenza logica della base di conoscenza ?

    RISPOSTA: vero, perché FC è completa rispetto a clausole di Horn e 
    la base di conoscenza considerata è composta di clausole di Horn.

(d) BC restituisce vero se gli si presenta la query P(b) ? spiegare perché. 

    RISPOSTA: No, perché cade in un ciclo infinito applicando la prima
    regola ripetutamente.

(e) se BC fallisce ad inferire un dato letterale, è vero concludere
    che tale letterale non è conseguenza logica della base di conoscenza ?

    RISPOSTA: No. Si consideri, ad esempio, cosa succede per P(b).


Esercizio 3

Date le sentenze
    s1: \forall x,y,l (S(x,l) AND S(y,l)) => U(x,y)
    s2: \forall x,y,l (S(x,l) AND S(y,l)) => (U(x,y) AND U(y,x))
dimostrare formalmente che s1 |= s2.

    RISPOSTA: se s1 |= s2, allora (s1 AND ¬s2) conduce ad una contraddizione.
    Trasformiamo s1 e ¬s2 in CNF:
    s1:  ¬S(x,l) OR ¬S(y,l) OR U(x,y)
    ¬s2: ¬(\forall x,y,l (S(x,l) AND S(y,l)) => (U(x,y) AND U(y,x)))
         \exist x,y,l ¬( ¬(S(x,l) AND S(y,l)) OR (U(x,y) AND U(y,x)))
         S(M1,M3) AND S(M2,M3) AND (¬U(M1,M2) OR ¬U(M2,M1))
    dove M1, M2, M3 sono costanti di skolem e quindi (s1 AND ¬s2) da origine 
    alle forme:
    Q1: ¬S(x,l) OR S(y,l) OR U(x,y)
    Q2: S(M1,M3)
    Q3: S(M2,M3)
    Q4: (¬U(M1,M2) OR ¬U(M2,M1)) 
    Per mostrare la contraddizione, applichiamo la risoluzione.
    - risolvendo Q1, Q2, {x/M1, l/M3}, otteniamo Q5: ¬S(y,M3) OR U(M1,y)  
    - risolvendo Q5, Q3, {y/M2}, otteniamo Q6: U(M1,M2)
    - risolvendo Q1, Q2, {y/M1, l/M3}, otteniamo Q7: ¬S(x,M3) OR U(x,M1)  
    - risolvendo Q7, Q3, {x/M2}, otteniamo Q8: U(M2,M1)
    - risolvendo Q6, Q4, {}, otteniamo Q9: ¬U(M2,M1)
    - risolvendo Q8, Q9, {}, otteniamo la clausola vuota



Esercizio 4

Si può utilizzare in ogni caso la risoluzione per dimostrare
che per una data sentenza nella logica del primo ordine A esiste 
almeno un modello ?

    RISPOSTA: No. Se A è valida, allora la risoluzione applicata
    a CNF(¬A) termina con la clausola vuota. Se A è insoddisfacibile, 
    allora la risoluzione applicata a CNF(A) termina con la clausola 
    vuota. Ma se A è soddisfacibile, ne' la prima, ne' la seconda
    applicazione della risoluzione necessariamente terminano.



Esercizio 5

Mostrare che le sentenze 
A: \forall x [\forall y P(x,y)] => Q(x)
B: \forall x \exist y [P(x,y) => Q(x)]
sono logicamente equivalenti, convertendole in CNF e mostrando
tutti i passi di conversione.

    RISPOSTA: 
    A:  \forall x ¬[\forall y P(x,y)] OR Q(x)
        \forall x [\exist y ¬P(x,y)] OR Q(x)
        \forall x \exist y ¬P(x,y) OR Q(x)
    qui bisogna inserire una FUNZIONE di skolem (f(x)) per y 
    perché è all'interno dello scope di un quantificatore 
    universale
        ¬P(x,f(x))] OR Q(x)

    B:  \forall x \exist y [¬P(x,y) OR Q(x)]
        \forall x \exist y ¬P(x,y) OR Q(x)
    qui bisogna inserire una FUNZIONE di skolem (f(x)) per y 
    perché è all'interno dello scope di un quantificatore 
    universale
        ¬P(x,f(x))] OR Q(x)