L’automated reasoning studia tecniche per determinare automaticamente se una congettura phi e conseguenza logica di un insieme S di assunzioni.
Il problema tipico e: dato un sistema, un protocollo, un circuito, un programma o una struttura matematica, voglio verificare se una certa proprieta vale. S descrive cio che so dell’oggetto; phi descrive la proprieta da verificare.
Definizione
La knowledge representation e il problema collegato di scegliere formalismi adatti a rappresentare aspetti del mondo, come azioni, spazio, tempo, eventi mentali e ragionamento di senso comune.
Esempio: per un protocollo di comunicazione, S puo descrivere messaggi, chiavi e regole di transizione; phi puo dire che un segreto non viene mai rivelato.
Note
L’automated reasoning non e solo matematica: e uno strumento per costruire sistemi piu affidabili, spiegabili e verificabili.
Theorem Proving
Definizione
Il theorem proving e la ricerca di una prova che phi segua logicamente da S.
Si distingue tra:
Deductive theorem proving: verifica S |= phi.
Inductive theorem proving: verifica che S implichi tutte le istanze ground di phi.
Fully automated theorem proving: la macchina cerca la prova da sola.
Interactive theorem proving: umano e macchina collaborano.
Molte tecniche sono refutational: per dimostrare S |= phi, provano che S insieme a not phi e inconsistente. Se assumere il contrario porta a contraddizione, allora phi segue da S.
Esempio: in logica di programma, per provare che una funzione non produce mai output negativo, si aggiunge l’ipotesi “produce output negativo” e si cerca una contraddizione con specifica e codice.
Limite
In first-order logic il theorem proving deduttivo e semi-decidibile: se la prova esiste, una procedura puo trovarla; se non esiste, la procedura puo non terminare.
Decidibilita e SAT
Definizione
Un problema e decidibile se esiste una procedura che termina sempre con risposta corretta; semi-decidibile se termina garantitamente solo nei casi positivi.
In logica del primo ordine, la dimostrazione deduttiva e semi-decidibile. In logiche di ordine superiore diventa ancora piu difficile. Per questo il ragionamento completamente automatico si concentra spesso su frammenti decidibili.
Definizione
SAT e il problema di decidere se una formula proposizionale e soddisfacibile, cioe se esiste un’assegnazione di verita che la rende vera.
SAT e decidibile ma NP-complete. Molti problemi informatici possono essere codificati in logica proposizionale e dati a SAT solver, ad esempio bounded model checking.
Il metodo classico e DPLL: esplora assegnazioni di verita, propaga conseguenze e fa backtracking quando incontra conflitti.
Punto Essenziale
Decidibile non significa facile. Anche con garanzia di terminazione, il costo puo crescere in modo esplosivo.
Ragionamento come Ricerca
Definizione
Un metodo di automated reasoning combina un sistema di inferenza con un piano di ricerca.
Il sistema di inferenza definisce quali passaggi sono corretti: espansione per generare conseguenze, contrazione per eliminare o semplificare formule ridondanti. Il piano di ricerca decide quale regola applicare, a quali dati e in quale ordine.
Questa distinzione e cruciale:
Il sistema di inferenza definisce lo spazio delle prove possibili.
Il search plan trasforma quello spazio non deterministico in una procedura concreta.
Esempio: due theorem prover possono usare regole logicamente equivalenti, ma uno trova la prova in secondi e l’altro diverge, solo per differenze nella strategia di ricerca.
Note
Soundness significa che cio che produco e corretto; refutational completeness significa che, se c’e inconsistenza, il sistema puo derivare una contraddizione.
Logiche Non Classiche
Definizione
Le logiche non classiche estendono o modificano la logica classica per rappresentare fenomeni come tempo, possibilita, conoscenza, azioni, incertezza e ragionamento rivedibile.
Molti problemi AI non si rappresentano bene solo con logica classica. Le slide citano logiche modali, temporali, descrittive e non monotone.
Definizione
Il ragionamento non monotono permette conclusioni rivedibili: aggiungendo nuove informazioni, conclusioni precedenti possono diventare non valide.
In Prolog, la negation as failure e un esempio: not G ha successo se G non puo essere provato. Se in seguito aggiungo fatti che provano G, allora not G fallisce.
Answer Set Programming estende questa idea: un programma puo avere zero, uno o molti answer set, ciascuno interpretabile come un possibile mondo.
Esempio
open :- not closed.closed :- not open.
Il programma ammette due mondi possibili: {open} e {closed}.
L’Abductive Logic Programming introduce invece abducibles: ipotesi assumibili per spiegare osservazioni, vincolate da integrity constraints.
Model Checking
Definizione
Il model checking e una tecnica automatica per verificare sistemi a stati finiti controllando se una proprieta logica vale nel modello del sistema.
Il processo e:
Tradurre il sistema in un modello a stati e transizioni.
Specificare la proprieta phi, spesso in logica temporale.
Verificare se phi vale nel modello.
Esempio: in un sistema concorrente posso verificare che “ogni richiesta prima o poi riceve risposta” oppure che “due processi non entrano mai insieme nella sezione critica”.
Per sistemi multi-agente il problema si arricchisce: non basta il tempo, servono anche atteggiamenti mentali come conoscenza, credenze, desideri e intenzioni. Questo porta a combinare logiche temporali e modali.
Sfida
Il model checking soffre spesso di state explosion: il numero di stati cresce rapidamente con componenti concorrenti e variabili.
Applicazioni
Definizione
Le applicazioni dell’automated reasoning includono verifica, sintesi, pianificazione, programmazione dichiarativa, web semantico e sistemi multi-agente.
In hardware e software verification, theorem prover e model checker verificano protocolli crittografici, sistemi message-passing e specifiche software. In AI, tecniche di reasoning supportano planning, learning e natural language understanding.
Per il ragionamento sulle azioni, il situation calculus rappresenta situazioni come stati del mondo e azioni come trasformazioni. I fluents sono predicati che cambiano da una situazione all’altra. Una formula come p(s) -> q(result(a,s)) dice: se p vale in s, allora dopo l’azione a vale q.
Il frame problem resta critico: specificare in modo efficiente cosa non cambia dopo un’azione e difficile.
Nel Semantic Web, RDF e OWL permettono di esprimere conoscenza tramite ontologie; il reasoning verifica conseguenze, classificazioni e consistenza. Nei web services, il reasoning puo aiutare composizione, orchestrazione e coordinamento.