Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
Scarica il documento per vederlo tutto.
vuoi
o PayPal
tutte le volte che vuoi
Conseguenza logica e validità
R Q R ⇒ Q valida. Ovvero, Q è conseguenza logica di R se e solo se R implica Q è valida (ovvero è una tautologia). Dunque, per verificare che: KB ⇒ P1. Posso dimostrare che è una formula valida, cioè KB ⇒ P è vera in ogni modello, enumerando i modelli (costoso, è il model checking).
2. Equivalentemente, grazie a come è definita una tautologia, posso dimostrare per inferenza sintattica (ovvero manipolando le formule senza costruire modelli) che (KB ⇒ P) è True. Questo mi permette di ragionare tramite manipolazione sintattica, anziché dover operare tramite i modelli.
L'inferenza sintattica mi permetterà anche di ragionare per refutazione (o per assurdo). Questo è possibile grazie al fatto che A è valida se e solo se A è insoddisfacibile. ¬la validità dell'implicazione applicando la negazione e dimostrando l'insoddisfacibilità della formula.
ottenuta:equivalente a∨(R &=⇒ Q) (¬R &Q) negata diventa: ¬(¬R && Q) che è equivalente a per De Morgan ∧ ¬Q)(R Dimostrando l'invalidità di ∧ ¬Q)(R R &=⇒ Q Dimostrazione per refutazione Date due formule R e Q, se e solo se è |= ∧ ¬Q)(R Q) (Rinsoddisfacibile. Ragiono sulla negazione perché mi risulta più semplice con gli strumenti che utilizzerò, ovvero le regole di inferenza. Procedo per assurdo: nego la tesi (Q) e la aggiungo alle ipotesi (R). Se così facendo raggiungo una formula insoddisfacibile, la tesi era corretta e è valida. R &=⇒ Q Per verificare che |=KB P 611. Assumo per assurdo che ¬P2. Dimostro che è insoddsifacibile, ovvero che è in con-∧ ¬P ¬PKB traddizione con gli assiomi noti. Per raggiungere la contraddizione uso tecniche di manipolazione sintattica. Questa dimostrazione è del tutto analoga ad unaricerca nello spazio degli stati.
13.6 Formulazione come problema di ricerca nello spazio degli stati
Stato iniziale: background Knowledge.
Azioni (costruzione dei successori): regole di inferenza
Nodo obiettivo: stato che contiene la formula da dimostrare.
Importante
Questo vale solo per logiche monotone, ovvero le logiche tali per cui la conoscenza permane e aumenta, ma non diminuisce mai. Nessuna aggiunta di informazione invalida le conclusioni precedenti.
|= ∧ |=(KB P ) =⇒ (KB Q P )
La dimostrazione avviene coniugando:
Un algoritmo di ricerca, che usa le regole di inferenza per costruire i successori
Un insieme di regole di inferenza (che suppongo siano corrette e complete)
13.7 Regola di risoluzione
È una regola di inferenza, detta che: risoluzione
Unita a qualsiasi algoritmo di ricerca (ovvero se esistono soluzioni ne trova una)
Produce un algoritmo di inferenza corretto e completo
Risoluzione (o resolution) permette di realizzare dimostrazioni per
Il tuo compito è formattare il testo fornito utilizzando tag html. ATTENZIONE: non modificare il testo in altro modo, NON aggiungere commenti, NON utilizzare tag h1; Il testo formattato con i tag html è il seguente:refu-sia in logica proposizionale che in logica del prim'ordine.
Nella resolution tutte le formule coinvolte sono clausole, ovvero disgiunzioni di letterali.
Ogni letterale compare una volta sola.
La fattorizzazione è quando i letterali complementari presenti nelle formule di partenza scompaiono nella formula risolvente.
Caso particolare:
Se nelle formule di partenza ho solo P e non P, otterrò come risultato l'assurdo (clausola vuota, è sicuramente falso).
Visto che a resolver si possono sottoporre solo clausole, tutte le formule vanno trasformate in CNF. Lo stesso vale per le implicazioni e biimplicazioni: vanno trasformate sfruttando le equivalenze sintattiche.
Data una qualsiasi formula proposizionale, esiste una congiunzione di clausole (CNF) ad essa equivalente.
Algoritmo di traduzione in clausole:
- Eliminare la biimplicazione ⇐⇒ ≡ ∧(a b) (a =⇒ B) (b =⇒a)
- Eliminare l'implicazione: ≡ ∨(a =⇒ b) (¬a b)
Portare tutti i not all'interno, applicando De Morgan. Distribuire l'or sull'and dove possibile
Tutta la KB va tradotta in clausole. Tutte le clausole della KB sono implicitamente valide contemporaneamente (sono tutte in and, senza che venga specificato).
Teorema: completezza della risoluzione
Se un insieme di clausole è insoddisfacibile, la chiusura della risoluzione contiene la clausola vuota.
Se la chiusura non risulta vuota, pur combinando tutte le clausole presenti nell'insieme, allora l'insieme è vero.
Se la chiusura dell'insieme delle clausole risulta vuota, e dunque insoddisfacibile, la risposta a sarà true, perché la chiusura noi |= KB Pl'avremo fatta con , dimostrando che è insoddisfacibile, dunque ¬P KB =⇒ sarà valida.
13.8 Clausole di Horn
Sono un sottoinsieme delle clausole, che, grazie alla loro formulazione, permettono meccanismi di inferenza che operano in tempo lineare o anche
inferiore. Denizione Una clausola di Horn è una disgiunzione di letterali in cui al più uno è positivo. Se esattamente un letterale è positivo (ovvero non negato), è detta clausola denita. Catturano le implicazioni la cui formula implicante è una congiunzione di letterali positivi, e la formula implicata è un singolo letterale positivo. Es: ∧ ≡ ¬A ∨ ¬B ∨A B =⇒ C C Consentono di vericare la consequenzialità logica in un tempo che cresce linearmente con la dimensione della KB. 13.8.1 Forward Chaining Permette di derivare una query data da un singolo simbolo proposizionale iniziale, partendo da una KB costituita da sole clausole di Horn. Procedimento: 1. Si parte dai fatti conosciuti 2. Si applica il modus ponens ( ) e dunque non il meccanismo di risoluzione 3. Se tutte le premesse di un'implicazione sono vere, si aggiunge la conseguenza ai fatti noti 4. Terminazione: o si ottiene la query (restituendo true), oppure nonSi possono fare altre inferenze e viene restituito false. Ha complessità lineare nella dimensione di KB, perché le regole di inferenza vengono applicate al più una volta sola, concatenandole.
Importante
Per applicare regole di inferenza, ho bisogno di conoscenze di partenza. Se le conoscenze che ho non bastano per applicare nessuna regola, devo restituire false.
Esempio 1:
Regole: A ∧ B =⇒ C, C ∧ D =⇒ E
Fatti noti: A, D.
In questo caso i fatti noti non bastano per applicare nessuna regola.
Riguardo il Forward Chaining:
Ha complessità lineare.
È completo.
È inconscio: guidato dai dati e non usa informazione relativa ai goal.
Può attivare molte inferenze inutili ai fini della dimostrazione della formula in oggetto.
13.8.2 Backward chaining
È focalizzato, a differenza dell'FC.
Parte dalla formula da dimostrare, non dai fatti noti.
Se essa risultasse già vera, restituirebbe true. Altrimenti cerca le clausole.
diHorn di cui la formula da dimostrare è conclusione, ovvero, procede aritroso no a giungere ai fatti noti.Cerca solo quello che gli serve, non attiva inferenze inutili.
Riguardo il Backward Chaining:
Realizza una forma di ragionamento guidata agli obiettivi
È usato nel theorem proving e nella programmazione logica come meccanismo di inferenza
Spesso è più efficiente del forward chaining (in quanto è focalizzato), è meno che lineare.
Implementazione
Il Backward Chaining può essere implementato come uno stack:
Inizialmente faccio il push della formula da dimostrare
Estraggo il top, e controllo se è un fatto noto:
Se lo è, restituisco true. Altrimenti faccio il push sullo stack delle formule che decidono la verità di quella che ho appena estratto.
Quando arrivo ad avere lo stack vuoto, non ho più elementi da controllare, dunque fornisco la risposta true o false.
14 Logica del prim'ordine. È necessaria
La logica proposizionale è un sistema formale utilizzato per rappresentare oggetti del mondo in relazione fra di loro. In generale, parte dalla logica proposizionale e ne aumenta l'espressività. Punti di forza della logica proposizionale:
- È dichiarativa: separa nettamente conoscenza da inferenza, distinguendo cosa sa da cosa deriva. È un vantaggio perché permette la realizzazione di meccanismi di inferenza automatici e generali.
- Consente di derivare fatti da altri fatti. La sua semantica è data da una relazione di verità che collega formule e mondi possibili (modelli). Il significato di una formula è ottenuto componendo il significato delle sue parti. Posso operare sulle singole parti, anche questo contribuisce a realizzare l'automatismo.
- Non è ambigua: è vera o falsa, non ci sono dubbi o incertezze. Questa è una caratteristica molto importante.
Limiti della logica proposizionale:
- Non sono tutte le problematiche risolte dalla logica del
prim'ordine):La logica proposizionale non permette rappresentazioni compatte. .Non permette di codicare espressioni generali Non permette di esprimere relazioni fra elementi In generale, , in quanto ogni oggetto/elementomanca di espressività rappresentato deve avere un suo specico simbolo.È necessario introdurre nuovi strumenti/simboli per ottenere la generalità ele relazioni fra elementi, non sono sucienti i simboli messi a disposizionedalla logica proposizionale.
Voglio mantenere le buone caratteristiche della logica propo-sizionale, ed aggiugere ad esse delle soluzioni per le mancanze de-In particolare, voglio poter esprimere relazioni fra oggetti.scritte.
ImportanteNella logica del prim'ordine, il mondo è fatto di oggetti in relazione fradi loro, ed una relazione può essere vericata oppure no.Cambia la nozione di : non è più un'attribuzione di valori allemodellovariabili.Modello del prim'ordineContiene un
ed un' interpretazione. Il dominio a sua volta è formato da un insieme di oggetti e dalle relazioni fra tali oggetti. Elementi della logica del primo ordine:Simboli di costante
Simboli di predicato
Simboli di funzione
Simboli di variabile
Connettivi (and, or, not)
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo
