Dipartimento di Ingegneria informatica, automatica e gestionale

La ricerca svolta da Paolo Liberatore è concentrata sui formalismi logici per la rappresentazione della conoscenza in intelligenza artificiale, e su argomenti di complessità computazionale. In particolare ha lavorato sui seguenti temi.

Belief Revision (revisione della conoscenza). Questo è stato anche l'argomento principale della tesi di laurea. La tesi contiene in particolare la proposta di un operatore commutativo per l'integrazione di informazioni provenienti da varie fonti, ognuna con un uguale livello di plausibilità. Estratti della tesi sono stati pubblicati. Il primo articolo pubblicato contiene un algoritmo efficiente per la revisione della conoscenza. Questo algoritmo, a partire da una descrizione della base di conoscenza in forma clausale, identifica un possibile modello da eliminare, e in base a questa scelta rimuove dalla base di conoscenza le clausole che sono soddisfatte da questo modello. Un aspetto importante dei formalismi logici è quello della correlazione esistente fra essi. Questo permette la definizione di proprietà generali, e il riuso di algoritmi proposti in un formalismo in altri formalismi. Un articolo su conferenza poi pubblicato su rivista contiene una serie completa di riduzioni dal problema della revisione della conoscenza a quello della cirumscription, e viceversa. Dal momento che tutte queste riduzioni sono polinomiali, questo permette appunto di utilizzare algoritmi sviluppati per uno dei due formalismi nell'altro. Una simile correlazione fra il problema del belief update e quello della assunzione di mondo chiuso è stata stabilita: molti dei formalismi per l'aggiornamento della conoscenza che sono stati proposti per risolvere questo problema nel caso di formule disgiuntive sono riconducibili a opportuni formalismi introdotti precedentemente per la trattazione della assunzione di mondo chiuso. Una variante della revisione è stata introdotta, ed è stato presentato un formalismo generale di fusione di basi di conoscenza con lo stesso grado di priorità. Una definizione e implementazione di un sistema in grado di effettuare allo stesso tempo fusione, revisione e aggiornamento è stata poi realizzata. La generalizzazione di revisione, arbitraggio e aggiornamento ha portato all definizione di una semantica che consente il trattamento di problemi che comportano l'uso di tutti e tre gli operatori. Questa semantica è stata successivamente implementata.

Abduzione Uno dei problemi considerati è quello di trovare un insieme minimo di test che permettono di identificare univocamente una spiegazione abduttiva. Questo problema è applicabile a tutti i problemi di tipo diagnostico che si possono codificare in termini di abduzione, dal momento che lo scopo della diagnosi è quello di identificare univocamente le cause di un insieme di manifestazioni. L'abduzione è spesso usata per formalizzare problemi in cui la teoria logica, e gli insiemi di ipotesi e di (possibili) manifestazioni sono noti in anticipo, mentre l'insieme di manifestazioni effettivamente osservate può risultare noto molto piu'u tardi. Per problemi di questo tipo una precompilazione della parte di input nota in anticipo puè risultare vantaggiosa; questo tipo di strategia è stata quindi analizzata.

Computational Complexity (complessità computazionale). In questo campo, Paolo Liberatore ha lavorato essenzialmente alle proprietà computazionali della teoria delle azioni e del cambiamento. L'analisi computazionale è utile per determinare l'esatto grado di difficoltà dei problemi in intelligenza artificiale. Una prima analisi ha riguardato la complessità della revisione della conoscenza, nel caso in cui è richesta una sequenza di revisioni invece che una revisione singola. In seguito è stata studiata la complessità del belief update e del problema della ridondanza. Un problema centrale nello studio di complessità è quello della verifica di modelli, di cui è stato condotto uno studio sistematico di complessità, dimostrando tra le altre cose come la complessità del problema di verifica dei modelli può differire dalla complessità della implicazione. A rulstati simili risultati è anche giunta l'analisi della complessità della verifica dei modelli in sulla logica dei default: restrizioni della logica che hanno la stessa complessità di inferenza presentano invece proprietà differenti quando si considera il problema della verifica dei modelli. Dal momento che esistono molte semantiche diverse per default logic, è utile analizzare le teorie che hanno una interpretazione unica. Il loro studio consente di estendere dei risultati a più semantiche. Un altro studio di complessità ha riguardato il ragionamento sulle azioni, dimostrando che il formalismo base proposizionale è NP-completo. Questo implica che, sebbene il problema sia da considerarsi difficile, esistono delle tecniche algoritmiche che potrebbero consentirne la soluzione. In particolare, si dimostra la possibilità di utilizzare algoritmi per la soddisfacibilità di formule proposizionali, mostrando una traduzione molto semplice dalla logica delle azioni a quella proposizionale. Un problema simile, ma molto più complesso, è quello delle logiche lineari temporali. In questo caso, si è mostrata una traduzione da QBF a queste logiche, che produce vari benefici, fra cui la possibilità di risolvere problemi di QBF usando risolutori di logica noti, e quello di generare problemi difficili in modo casuale. Uno studio di complessità del problema della pianificazione automatica ha riguardato il problema della ripianificazione, ossia della costruzione di un piano qualora un piano precedentemente noto risulti non più valido a causa di un cambiamento degli obiettivi da raggiungere o di una scoperta di errori nella descrizione dello stato iniziale. Riguardo al problema della soddisfacibilità di vincoli, è stata considerata la complessità e la approssimabilità del problema di trovare un insieme massimale di variabili che soddisfino i vincoli. La complessità teorica dell'algoritmo di Davis, Putnam, Logemann e Loveland è stata analizzata, dimostrando che la complessità di determinare in modo ottimo la variabile su cui fare branching (tale scelta è una parte dell'algoritmo) è computazionalmente più difficile del problema che si vuole risolvere. La immediata conseguenza di questo risultato è che non è sensato indirizzarsi verso la scelta ottima, ma che effettuare scelte non ottime è in generale necessario. Questo risultato è stato poi esteso, in un successivo articolo, al caso in cui il branching è limitato a un insieme di variabili e all'algoritmo di risoluzione. Altre analisi hanno riguardato la unicità delle estensioni nella teoria dei default e problemi la dipendenza fra variabili nella logica proposizionale.

Compilabilità e rappresentazioni compatte Questa è una nuova applicazione della complessità computazionale. Il punto di partenza di questo studio è stata la definizione di due generachie di classi di problemi che formalizzano il livello di difficoltà di problemi in cui una compilazione di parte dell'input è permessa. Lo studio della possibilità di ridurre la complessità del problema in questo modo è stata poi portato avanti, considerando problemi differenti come la diagnosi, la pianificazione automatica, il ragionamento su azioni e la revisione della conoscenza. I Markov Decision Process, che formalizzano problemi di pianificazione in situazioni di incertezza, sono stati in seguito considerati. A partire dalla formalizzazione delle classi di compilabilità è possibile dimostrare risultati sulla rappresentazione succinta informazioni in formalismi logici. Dimostrazioni di non-compilabilità possono venire sfruttate per dimostrare che alcuni formalismi proposizionali sono in grado di rappresentare l'informazione in minore spazio. È stata analizzata la possibilità di rappresentare il risultato di una revisione in forma compatta. Questo problema è stato poi considerato anche nel caso in cui la informazione sia rappresentata in forma di clausole di Horn. Il problema della rappresentazione compatta di politiche per i processi di decisione markoviani (MDP), che sono problemi di pianificazione probabilistica, è in seguito analizzato.