Paracoherent Answer Set Programming

Abstract

L’Answer Set Programming (ASP) è un paradigma di programmazione dichiarativa basato sulla semantica dei modelli stabili. L’idea alla base di ASP è di codificare un problema computazionale in un programma logico i cui modelli stabili, anche detti answer sets, corrispondono alle soluzioni del problema originale. La semantica degli answer sets potrebbe non assegnare alcun modello ad un programma logico a causa di contraddizioni logiche o di negazioni instabili, causate dalla dipendenza ciclica di un atomo dal suo negato. Mentre le contraddizioni logiche possono essere gestite con le tecniche tradizionali usate nel ragionamento paraconsistente, l’instabilità della negazione richiede altri metodi. Ricorriamo qui ad una semantica paracoerente in cui sono utilizzate delle interpretazioni a 3 valori, dove un terzo valore di verità, oltre a quelli classici di vero e di falso, esprime che un atomo è creduto vero. Ciò è alla base della semantica dei modelli semi-stabili che è stata definita attraverso l’utilizzo di una trasformazione del programma originario. Questa tesi ha come punto di partenza un articolo presentato nel 2010 alla dodicesima “International Conference on Principles of Knowledge Representation and Reasoning” [21], dove viene offerta innanzitutto una caratterizzazione dei modelli semi-stabili che rende la semantica più comprensibile. Inoltre, motivati da alcune anomalie di tale semantica rispetto ad alcune fondamentali proprietà epistemiche, viene proposta una correzione che soddisfa queste proprietà. Per questa nuova semantica viene offerta sia una definizione attraverso una trasformazione del programma originario che una caratterizzazione teorica dei modelli, che si rivelano essere un rilassamento della logica di equilibrio, una logica caratterizzante la semantica degli answer sets. Pertanto, la semantica introdotta viene chiamata semantica dei modelli di semi-equilibrio. Nella tesi consideriamo alcuni miglioramenti di questa semantica rispetto alla modularità nelle regole del programma, basata sugli insiemi di splitting, il principale strumento per la modularità usato nel modellare e nel valutare i programmi ASP. Tra questi selezioniamo classi di modelli canonici che permettono una valutazione bottom-up dei programmi ASP, con l’opzione di passare ad una modalità paracoerente quando si rileva la mancanza di un answer set. L’analisi della complessità computazionale dei principali task di ragionamento mostra che i modelli di semi-equilibrio sono computazionalmente più difficili rispetto agli answer sets (ovvero, modelli di equilibrio), a causa di una minimizzazione globale necessaria per mantenere quanto più piccolo possibile il gap tra atomi creduti veri e atomi veri. Successivamente consideriamo differenti algoritmi per calcolare modelli semi-stabili e modelli di semi-equilibrio, implementandoli ed integrandoli all’interno di un framework per la costruzione degli answer sets. Riportiamo poi i risultati di esperimenti condotti sui benchmarks provenienti dalle ASP competitions, identificando l’algoritmo più efficiente. I risultati di questa tesi contribuiscono alla fondazione logica dell’ASP paracoerente, che sta gradualmente ottenendo una maggiore importanza nella gestione delle inconsistenze e, allo stesso tempo, offrono una base per lo sviluppo di algoritmi e per la loro integrazione all’interno di un solver ASP.