Research activity in 1996
L'attività di ricerca è stata svolta prevalentemente nell'ambito
dei progetti MURST 40% "Rappresentazione della conoscenza e meccanismi di
ragionamento", CNR "Ambienti e strumenti per la gestione di informazioni
temporali" e ESPRIT BRA Medlar II, concluso all'inizio del 1996. Alcune
ricerche si sono anche svolte nell'ambito di progetti bilaterali con
l'Università di Marsiglia e con l'Imperial College di Londra.
Per quanto riguarda la programmazione logica, l'attività di
ricerca è stata principalmente rivolta alla definizione di estensioni
delle clausole di Horn che ne aumentino il potere espressivo senza
pregiudicarne la chiarezza semantica e la dichiaratività. In
particolare, si sono affrontate le seguenti tematiche:
- estensioni modali,
- ragionamento ipotetico,
- ragionamento su azioni,
- abduzione.
Tutti i punti, tranne il primo, coinvolgono problematiche di ragionamento
non-monotono.
(1) E' stata definito un contesto per lo sviluppo di estensioni modali della
programmazione logica, parametrico rispetto alle proprietà delle
modalità scelte. In particolare, i linguaggi di tale contesto consentono
di utilizzare modalità del tipo [t], dove t è un termine del
linguaggio, di fronte all'intera clausola, al goal oppure alla testa di una
clausola. Le proprietà delle modalità sono specificate da un
insieme di assiomi di inclusione, per mezzo dei quali è possibile
rappresentare la maggior parte dei sistemi modali noti. I linguaggi
appartenenti al contesto definito consentono di eseguire ragionamento
epistemico, di definire moduli annidati e parametrici, di descrivere
ereditarieta` tra classi e di ragionare sulle azioni. La caratteristica
rilevante di tale contesto è che la procedura di prova è
modulare, ossia è unica per tutti i linguaggi in esso definibili, e
può essere adattata alle proprietà delle particolari
modalità sfruttando una relazione di riscrittura che è funzione
degli assiomi scelti.
(2) Per quanto riguarda il ragionamento ipotetico, è stato definito un
linguaggio di programmazione logica che permette di fare aggiornamenti
ipotetici in presenza di vincoli e possiede meccanismi di revisione delle
credenze che mantengono la base di conoscenza consistente. Tale linguaggio
permette di ragionare su basi di conoscenza priorizzate e di aggiornarle e
fornisce gli strumenti per fare ragionamento di tipo condizionale,
controfattuale e non-monotono. Per esso sono state definite una semantica
abduttiva ed una procedura di prova diretta dal goal che calcola le soluzioni
abduttive. Sono state inoltre studiate le relazioni fra questo linguaggio
ipotetico e le logiche condizionali.
(3) La logica modale permette di formalizzare il ragionamento su azioni in modo
molto naturale, rappresentando le azioni come modalità. In questo
contesto è stato sviluppato un linguaggio di programmazione logica
modale, che estende il linguaggio A di Gelfond e Lifschitz, e permette di
trattare il problema della "ramificazione", facendo uso di relazioni "causali"
fra i fluenti. Tale linguaggio ha una semantica abduttiva e una procedura di
prova diretta dal goal. La logica modale è stata inoltre utilizzata, in
un ambito più generale, per definire una teoria delle azioni e del
cambiamento in cui la causalità viene rappresentata mediante un
opportuno operatore modale. In tale teoria la persistenza è ottenuta
mediante un formalismo nonmonotono, che massimizza le assunzioni di
persistenza. Oltre al problema delle ramificazioni vengono trattate le azioni
nondeterministiche, le situazioni con stato iniziale incompleto e
"postdiction".
(4) E' stata analizzata l'interpretazione abduttiva della negazione per
fallimento definendo una semantica a tre valori che generalizza la "semantica
dei modelli stabili". È stato inoltre adottato un approccio abduttivo
generale per modellare gli aspetti non-monotoni di linguaggi logici, proponendo
una procedura di prova diretta dal goal che calcola le soluzioni abduttive.
L'approccio è stato utilizzato per definire la semantica, e per
realizzare un interprete, dei linguaggi descritti ai punti (2) e (3).
Un altro tema di ricerca affrontato è quello della programmazione
logica e basi di dati. E' stato intrapreso, a partire dal Settembre 1995,
un rapporto di collaborazione scientifica col professor V.S. Subrahmanian,
dell'Università del Maryland (College Park), partecipando ad un
progetto per la definizione di un sistema mediato che integra diverse sorgenti
di dati eterogenee. Il meccanismo di integrazione è basato su di
un'istanza della programmazione logica con vincoli. L'integrazione di basi di
dati eterogenee, ciascuna associata ad una sua propria politica di protezione
di dati, comporta l'analisi di specifici problemi di sicurezza: il
sistema di integrazione deve infatti garantire il rispetto delle politiche di
sicurezza, sia di quelle locali alle varie basi di dati integrate, sia di
quella globale, imposta sulle relazioni risultanti dall'integrazione.
La Programmazione Logica in questa ricerca riveste due ruoli distinti. Da un
lato, come linguaggio di rappresentazione della conoscenza e meccanismo di
deduzione automatica computazionalmente trattabile, per risolvere il problema
di combinare ordinamenti di sicurezza eterogenei. Dall'altro, come strumento
per la definizione e l'uso di basi di dati, ed in particolare di viste derivate
(materializzate e non), che in questa ricerca viene arricchito di meccanismi
per mantenere la protezione dei dati durante interrogazioni ed aggiornamenti.
Sono stati studiati metodi di dimostrazione per svariati formalismi
logici. In particolare, sono state sviluppati sistemi alla Gentzen per la
logica dei default di Reiter, sia per la deducibilità ristretta ad una
singola estensione, sia per la deducibilità riguardo a tutte le
estensioni. Tali sistemi sono un punto di partenza promettente per realizzare
procedure deduttive efficienti e studiare strategie di ricerca di prove,
nonchè per ottenere un framework generale per la rappresentazione e lo
studio teorico di logiche nonmonotone.
In collaborazione con il gruppo del Prof. Mundici dell'Università di
Milano, si sono elaborate tecniche di dimostrazione automatica per la logica a
infiniti valori di Lukasiewicz. Più precisamente, si è formulato
un calcolo della risoluzione per un frammento di tale logica di cui si è
ottenuta una caratterizzazione in termini di funzioni di McNaughton, sono state
isolate classi di clausole per cui tali procedure risultano trattabili
(polinomiali), analoghe alle corrispondenti classi Horn e Krom del caso
classico. Sono stati sviluppati algoritmi di model building efficienti per
insiemi di clausole soddisfacibili. Questa ricerca avviene nell'ambito
dell'azione europea COST su Multiple-Valued Logic.
L'attività di questo gruppo ha stretti collegamenti con
l'attività svolta dal gruppo di Intelligenza Artificiale.
1996 Publications
M. Baldoni, L. Giordano and A. Martelli, Translating a Modal Language
with Embedded Implication into Horn Clause Logic, Proc. Int. Workshop on
Extensions of Logic Programming -- ELP'96, LNAI 1050, Springer Verlag,
19-33, 1996.
M. Baldoni, L. Giordano and A. Martelli, A Framework for Modal Logic
Programming, Proc. Joint Int. Conf. and Symp. on Logic Programming
(JICSLP'96), Bonn, Sept. 1996.
M. Baldoni, L. Giordano, A. Martelli and V. Patti, An abductive Proof Procedure
for Reasoning about Actions in Modal Logic Programming, JICSLP'96
Post-conference Workshop on Non-monotonic Extensions of Logic Programming,
Bonn, Sept. 1996.
P.A. Bonatti. Sequent Calculi for Default and Autoepistemic Logics. Proc.
TABLEAUX'96, LNAI 1071, 127-142, Springer-Verlag, 1996.
P.A. Bonatti, T.Eiter. Querying disjunctive databases through nonmonotonic
logics. Theoretical Computer Science 160:321-363, 1996.
P.A. Bonatti, M.L. Sapino, and V.S. Subrahmanian. Merging Heterogeneous
Security Orderings. Proc. ESORICS96 - International Symposium in the
computer security area, LNCS 1146, pp.183--197.
D.M. Gabbay, L. Giordano, A. Martelli and N. Olivetti, A Language for handling
Hypothetical Updates and Inconsistency, Journal of the Interest Group in
Pure and Applied Logic (IGPL), 4, (3), 1996.
L. Giordano, A. Martelli and M.L. Sapino, Extending Negation as Failure by
Abduction: a 3-valued Stable Model Semantics, Journal of Logic Programming,
26, (1),1996.
L. Giordano, A. Martelli and M.L. Sapino, An abductive Proof Procedure for
Conditional Logic Programming, Proc. 1st Int. Conf. on Formal and Applied
Practical Reasoning - FAPR'96, LNAI 1085, Springer Verlag, 231-245, 1996.
