Normal Form Nested Programs

Abstract

Nella Programmazione Logica Disgiuntiva (PLD) le regole sono costituite da una testa e da un corpo. La testa è una disgiunzione di atomi, mentre il corpo una congiunzione di letterali. La PLD, sotto la semantica degli Answer Set è ampiamente riconosciuta come importante strumento per la rappresentazione della conoscenza e del ragionamento non monotono. Lifschitz, Tang e Turner hanno esteso la semantica degli Answer Set (solo nel caso proposizionale o ground) ad una classe di programmi logici dove la testa e il corpo delle regole contengono espressioni innestate. Per espressioni innestate si intendono congiunzioni, disgiunzioni e negazione innestati arbitrariamente. Questa nuova classe di programmi è chiamata Programmi Logici Innestati e generalizza la classe dei programmi logici disgiuntivi proposizionali. Inoltre, è stato dimostrato che i programmi logici innestati possono essere trasformati in programmi logici disgiuntivi. Questi risultati ci permettono di valutare i programmi logici innestati usando i sistemi esistenti che supportano la PLD, come DLV, GnT, oppure Cmodels3. Si noti che le trasformazioni che consentono di ottenere i programma PLD introducono nuovi simboli e pertanto il programma risultante non è equivalente al programma originario nel senso classico. Ad ogni modo esiste una corrispondenza biunivoca tra gli answer set del programma innestato con gli answer set del programma trasformato. Sfortunatamente queste trasformazioni funzionano solo per programmi proposizionali e dunque non si possono usare le variabili, uno dei punti di forza dei programmi logici disgiuntivi. Questa limitazione diminuisce drasticamente l'applicabilità dei programmi logici innestati soprattutto quando il ragionamento è fatto su un numero molto grande di fatti. Una generalizzazione di queste tecniche a programmi che contengono variabili, non è ovvia. Per i programmi PLD l'indipendenza dal dominio è assicurata imponendo ai programmi delle condizioni sintattiche. Una di queste condizioni è nota come safety e per le regole PLD significa che ogni variabile che compare nella regola deve comparire anche in almeno un letterale positivo del corpo. Motivati da queste considerazioni, in questo lavoro di tesi estendiamo i programmi logici disgiuntivi non-ground ad una classe di programmi nei quali la testa delle regole è una formula in forma normale disgiuntiva composta da atomi, mentre il corpo è una formula in forma normale congiuntiva composta da letterali. Questi programmi sono chiamati programmi Normal Form Nested (NFN) e diversamente dai programmi logici innestati definiti da Lifschitz, Tang e Turner possono contenere variabili. In questo lavoro di tesi abbiamo studiato la semantica e la proprietà di indipendenza dal dominio e una trasformazione polinomiale dai programmi NFN ai programmi PLD, che preserva la safety. I principali contributi della tesi possono essere riassunti come segue. 1. Abbiamo esteso la DLP introducendo la congiunzione nella testa delle regole e la disgiunzione nel corpo delle stesse, ottenendo una nuova classe di programmi: i programmi NFN. 2. Abbiamo studiato le proprietà dei programmi NFN mostrando i seguenti risultati. a. Definita la Safety per i programmi NFN abbiamo dimostrato che ogni programma safe è indipendente dal dominio b. Gli answer set per i programmi NFN coincidono con gli answer set definiti da Lifschitz et al. per i programmi NLP, sul segmento del linguaggio comune. c. Gli answer set per i programmi NFN coincidono con i modelli stabili di Herbrand definiti da Ferraris et al. per le formule che corrispondono ai programmi NFN. d. Gli answer set per i programmi NFN coincidono con gli answer set per i programmi PLD definiti da Gelfond e Lifschitz. e. La nostra definizione di Safety per i programmi NFN è più generale di quella definita da Lee et al. sui programmi NFN. 3. Abbiamo progettato un algoritmo che trasforma i programmi NFN in programmi PLD in modo efficiente e abbiamo dimostrato che esso soddisfa importanti proprietà. a. La trasformazione preserva la safety. b. La taglia del programma trasformato è polinomiale nella taglia del programma NFN. c. Esiste una corrispondenza biunivoca tra gli answer set del programma NFN e quelli del programma riscritto. d. Abbiamo realizzato un sistema, nfn2dlp, che implementa l'algoritmo di riscrittura e un sistema che calcola gli answer set di un programma NFN: nfnsolve. Entrambi i tool sono disponibili al sito http://www.mat.unical.it/software/nfn2dlp/.; Università della Calabria