Metodi Formali nell'Ingegneria del Software

Progetti svolti dagli studenti

Torna alla lista dei progetti »

Verifica automatica di proprietà su ontologie DL-Lite A

• Autori: ,

• Categorie: Logica del primo ordine; Verifica di algoritmi, programmi, protocolli e hw; Otter/Prover9; Mace2; Dimostratori di teoremi al prim'ordine; Ricercatori di modelli al prim'ordine

Sommario

Questa relazione ha lo scopo di introdurre la Decription Logic "DL-Lite A", un sottoinsieme della First Order Logic particolarmente adatto a descrivere e ragionare su ontologie.
Nel capitolo 2 saranno descritte in dettaglio la sintassi e la semantica del linguaggio, i concetti di TBox (livello intensionale di una base di conoscenza) e ABox (livello estensionale di una base di conoscenza) e verrà mostrato superficialmente come si effettua il query answering su ontologie e quali sono i vantaggi di tale approccio.
Nel capitolo 3 mostriamo a puro scopo didattico, al fine di aiutare il lettore nella comprensione delle ontologie, la corrispondenza tra i classici diagrammi concettuali Entity Relationship (ER) e l'espressione dello stesso dominio in una ontologia DL-Lite A: questo procedimento di traduzione torna particolarmente utile qualora si vogliano migrare sistemi di basi di dati standard per cui è disponibile un diagramma concettuale in sistemi Ontology Based Data Access (OBDA).
Il capitolo 4 è invece il punto cruciale del lavoro: vogliamo mostrare come effettuare la verifica di proprietà statiche su un'ontologia espressa in DL-Lite A, ovvero rilevare eventuali inconsistenze o errori nella progettazione concettuale: allo stato attuale della ricerca, non esistono strumenti software che lavorano direttamente su DL-Lite A per effettuare verifica di proprietà statiche, se non banali. Mostreremo come, traducendo la base di conoscenza DL-Lite A in First Order Logic, sia possibile invece verificare qualsiasi proprietà esprimibile al primo ordine utilizzando strumenti preesistenti come il theorem prover OTTER e il ricercatore di modelli Mace. La sezione 5 è dedicata allo svolgimento di alcuni specifici casi di studio, per i diversi scenari illustrati ai capitoli 3 e 4. Nel primo esempio si mostra come a partire da una specifica in linguaggio naturale si progetta il diagramma ER che poi viene tradotto in formule di DL-Lite A. Il secondo esempio mostra come a partire da una ontologia in DL-Lite A si effettua la traduzione in FOL al fine di utilizzare Otter/mace per la verifica di proprietà.
Il sofware di traduzione automatica da DL-Lite A a FOL prende in input un'ontologia descritta in XML secondo il formato proprietario di QuOnto e la traduce in una base di conoscenza FOL scritta nel formato di Otter.

Materiale prodotto

• Slides

• Relazione

• Codice

Disclaimer: Questo materiale viene offerto gratuitamente ai soli studenti del corso di Metodi Formali nell'Ingegneria del Software del Corso di Laurea Specialistica in Ing. Informatica dell'Università degli Studi di Roma "La Sapienza". E' vietato ogni utilizzo diverso da quello inerente la preparazione dell'esame del suddetto corso, ed in particolare è espressamente vietato il suo utilizzo per qualsiasi scopo commerciale e/o di lucro.

Questo materiale è stato prodotto da un gruppo di studenti del predetto corso, e viene pubblicato senza alcuna garanzia, da parte del docente, circa la sua correttezza e completezza.

Il copyright di questo materiale è detenuto congiuntamente dagli autori e dal docente.
E' permessa la libera copia di tutto il materiale disponibile, purché ne vengano rispettate le condizioni d'uso qui enunciate, ne venga sempre citata la fonte, e venga riportato questo testo.
Gli autori consentono la stampa di questo materiale da parte di società di servizi (ad es. copisterie), purché queste non ne ottengano alcun ricavo oltre quello dovuto alla vendita di semplici fotocopie a prezzi di mercato. Si precisa tuttavia che gli autori ed il docente non percepiscono alcun guadagno dalla diffusione del materiale da parte di chiunque.