Scritto Del 6-7-risoluzione

Transcript

APPELLO DI MATEMATICA DISCRETA DEL 6-7-2015Prova di Logica (i quesiti contrassegnati con * riguardano solo gli studenti di Informatica) 1. La proprietà transitiva della inclusione insiemistica è: (AB  BC)  AC. a) mostrala intuitivamente con una rappresentazione grafica A B C b) tramite trasformazioni dimostrare che è equivalente alla formula BC ( AB  AC) Partendo da (AB  BC)  AC, questa è equivalente a ( AB  BC)  AC, per de Morgan equivalente a AB  BC  AC, e quindi BC  (AB  AC) e quindi BC  (AB  AC) e da qui la tesi c) tradurla in una formula della logica dei predicati, usando il predicato binario . (x (xA  xB)  x (xB  xC))  x (xA  xC) d) Dimostrare tale formula (tautologia) con la deduzione naturale. O la si dimostra come tautologia partendo dall’insieme vuoto di premesse o si usa il teorema di deduzione per scriverla come x (xA  xB), x (xB  xC)  x (xA  xC) x (xA  xB ) premessa x (xB  xC) tA premessa assunzione per -intro x (xA  xB) import tA  tB -elim tB -elim x (xB  xC) import tB  tC -elim tC -elim tA  tC export per -intro x (xA  xC) -intro e) * Dimostrarla con le tavole semantiche. x (xA  xB ) x (xB  xC) x (xA  xC) x (xA  xB ) x (xB  xC) (dA  dC) x (xA  xB ) x (xB  xC) dA  dC dA  dB dB  dC dA  dC x ……. dA dB dB  dC dB  dC dA  dC x …… dA  dC x …… dB dB dA  dC x …… dB dC dA  dC x ….. 2. a) Scrivere come formule della logica dei predicati (con uguaglianza) le frasi: “Solo 0 e 1 soddisfano l’equazione x2 = x.”, “Per il  vale la proprietà commutativa ed esiste l’elemento identico” x (x2 = x)  x=0  x=1 x y (xy = yx)  z x xz = zx = x b) skolemizzare la formula: x y z yz=zy=x, y yf(y)=f(y)y=c c) interpretare la  come il prodotto tra numeri, e usare come universo del discorso , e -{0}. In quali di queste interpretazioni la formula è soddisfatta, e perchè? Se l’universo del discorso è -{0} la formula è soddisfatta, l’interpretazione più ovvia si ha interpretando f(y)= c y-1 e c=1 (ma andrebbe bene ogni valore di c): Infatti lo 0 è l’unico elemento di  che non ammette inverso. Se invece l‘universo è  questa interpretazione non la soddisfa ma la formula viene soddisfatta da c=0 e f(y)=0. 3. Che cosa è il ‘general theorem prover’ (gtp)? Qual è un gtp nella logica delle proposizioni? E’ decidibile? *Conosci dei gtp nella logica dei predicati? Sono decidibili? Il gtp è un algoritmo che ha in input un sistema di assiomi e una formula e in output dice se la formula è dimostrabile o no dagli assiomi (è un teorema o no). Per la logica delle proposizioni il gtp è dato da una tavola delle verità: se in tutte le interpretazioni in cui sono soddisfatti gli assiomi la formula è soddisfatta allora la formula è dimostrabile (un teorema), ed il gtp è decidibile poiché l’algoritmo si ferma sempre. Per la logica dei predicati il gtp è dato dalle tavole semantiche (o dalla risoluzione): se la tavola semantica formata dagli assiomi e dalla negazione della formula è sempre chiusa, allora la formula è dimostrabile dagli assiomi (è un teorema). Il gtp è solo semidecidibile poiché possono crearsi rami infiniti di tavole aperte nel caso di risposta negativa. Usando la risoluzione applicata agli assiomi e alla negazione della formula, se si ricava una contraddizione la formula è un teorema, altrimenti no e l’algoritmo potrebbe anche non terminare (semidecidibilità).