Soluzionedellaprovadel21febbraio2019

Pagina 1

SOLUZIONE DELLA PROVA DEL 21/2/2019 Esercizio 1 (a) Per il teorema di correttezza e completezza forte , F si deduce nella teoria L dall’insieme {A, B, ¬B ¬C}se e solo se F si deduce semanticamente dallo stesso insieme. Gli unici modelli dell’insieme {A, B, ¬B ¬C}sono v1 e v 2 tali che v1(A) = v1(B) = v1(C) = 1 e v2(A) = v2(B) = 1 v2(C) = 0 che risultano essere modelli anche per F perciò possiamo affermare che esiste una deduzione di F dall’insieme dato. (b) Per provare il risultato ottenuto utilizzando la risol uzione utilizziamo il teorema di risoluzione e il teorema che lega la deducibilità semantica all’insoddisfacibilità, cioè F si deduce da {A, B, ¬B¬C} se e solo se {A, B, ¬B ¬C, ¬ F }è insoddisfacibile. Dobbiamo pertanto scrivere in clausole le formule dell’insieme {A, B, ¬B ¬C}e la formula ¬ F. Risulta: ¬B¬C ≡ B  ¬C ¬ F ≡ (¬A˅¬B˅¬C)˄(¬A˅¬B˅ C)˄(¬A˅B˅C) ≡ ((¬A˅¬B )˅(C˄¬C) )˄(¬A˅B˅C) ≡ (¬A˅¬B )˄(¬A˅B˅C) ≡ (¬A˅(¬B˄(B˅C))) ≡ (¬A˅(¬B˄C)) ≡ (¬A˅¬B)˄(¬A˅C) Le clausole di input allora sono C 1 = {A }, C 2 = { B}, C 3 = { B,¬C}, C 4 = {¬A,¬B }, C5 = {¬A, C }. Una derivazione per risoluzione della clausola vuota è la seguente: (I) C4 = {¬A,¬ B} (clausola di input) (II) C2 = { B} (clausola di input) (III) C6 = { ¬A} (risolvente di C4 e C2) (IV) C1 = {A} (clausola di input) (V) □ (risolvente di C6 e C1) Avendo ottenuto la clausola vuota si può concludere che F si deduce da {A, B, ¬B¬C}. Esercizio 2 (a) Condizione necessaria affinché esista la chiusura d’ordine di R è che R sia antisimmetrica. Ma la doppia freccia tra gli elementi 2 e 3 mostra che R non lo è. (b) Il grafo di incidenza di T = R2 è 1 3 4 2 5 Le funzioni contenute in T sono: f1= {(1,3),(2,2),(3,3),(4,2),(5,2)}, f2={(1,5),(2,2),(3,3),(4,2),(5,2)} f3= {(1,3),(2,2),(3,3),(4,3),(5,2)},…