Questo progetto di tesi si propone di implementare il metodo di ragionamento proposto nel lavoro Temporal Abductive Reasoning about Biochemical Reactions (Journal of Applied Non Classical Logics, to appear).
Il metodo consente di risolvere problemi di questo tipo: data una teoria di sfondo T ed un'osservazione E, che non è spiegata da T (cioè E non è una conseguenza logica della teoria), quali ipotesi è possibile aggiungere a T in modo che E sia conseguenza della nuova teoria così ottenuta?
La logica all'interno della quale si vuole eseguire questo tipo di ragionamento è la logica temporale lineare (LTL), per la quale però si ammettono formule di una forma sintattica ristretta. Le restrizioni sintattiche consentono tuttavia di dare una rappresentazione logica della conoscenza relativa alle interazioni tra i componenti biochimici di cellule e molecole, così come sono a volte rappresentate dai biologi mediante diagrammi chiamati Molecular interaction maps (MIM). Ragionare su tali complesse sequenze di interazioni può servire, ad esempio, nella ricerca sul cancro, per determinare come si può ottenere l'apoptosi (morte) di una cellula per mezzo dell'attivazione o inibizione di alcune proteine.
Un altro argomento di tesi in questo contesto consiste nella generazione delle formule LTL che rappresentino una determinata MIM.
Su questo tema è anche possibile fare lavoro di tipo teorico. Ad esempio, si possono esaminare diverse strategie di risoluzione utilizzate in logica classica, allo scopo di determinare quali di esse si possono riadattare alla logica temporale nel contesto della generazione di ipotesi, assicurando di derivare tutte quelle "interessanti".
Nel 2002 è stato implementato (in Objective Caml) il dimostratore GQML per logiche modali del primo ordine (con i quantificatori). Il sistema è stato presentato nell'articolo A General Theorem Prover for Quantified Modal Logics . Un lavoro successivo (Implementing and Evaluating Provers for First-order Modal Logics) tuttavia ha evidenziato che GQML ha dato in alcuni casi delle risposte non corrette.
Questo progetto di tesi si propone di riesaminare GQML alla luce dei risultati menzionati, ed eventualmente reimplementarlo, e di eseguire una serie di test su banchmark problems per le logiche modali del primo ordine (si vedano anche altri lavori che citano "A General Theorem Prover for Quantified Modal Logics").
Sibyl è un dimostratore automatico per la logica modale ibrida, arricchita con alcune caratteristiche tipiche delle Description Logics (DL). Sibyl è implementato in Objective Caml.
Le DL sono il nucleo di base dei dei linguaggi per la rappresentazione di ontologie, e sono, di fatto, una variante sintattica delle logiche modali. Si vedano, ad esempio:
Questo progetto di tesi si propone di estendere Sibyl in modo che possa comportarsi anche come dimostratore per le DL che può catturare, e di confrontare le sue prestazioni con quelle dei dimostratori esistenti per tali logiche.
La correttezza del dimostratore Sibyl di cui si è parlato nel punto precedente è stata controllata utilizzando una traduzione in logica classica del linguaggio accettato dal dimostratore, ed il prover SPASS. I test effettuati hanno anche consentito di comparare le prestazioni di Sibyl con quelle di SPASS. Sibyl si comporta in generale meglio di SPASS, tuttavia, i risultati ottenuti dipendono dalla traduzione usata, che è piuttosto semplice e diretta.
Questo progetto di tesi si propone di studiare e implementare meccanismi di traduzione più sofisticati (si veda ad esempio Translation Methods for Non-Classical Logics: An Overview) e di valutare le prestazioni di Sibyl utilizzando traduzioni ottimizzate.
Allo scopo di comparare il comportamento del dimostratore Sibyl presentato sopra, sono stati effettuati diverse serie di test su insiemi di formule generate casualmente. A questo scopo è stato utilizzato il generatore casuale di formule hgen, descritto in un articolo che si può scaricare da qui.
Purtroppo però al momento non si dispone di insiemi di test che contengano formule la cui difficoltà cresca in modo regolare.
Questo progetto di tesi si propone di esaminare il problema della generazione di benchmark per logiche modali in generale, e per la logica ibrida in particolare, determinando come si debbano stabilire nel modo più appropriato i parametri per la generazione casuale di formule.
Inoltre, dato che hgen non è più mantenuto da molto tempo, un altro obiettivo è quello di reimplementare un generatore casuale di problemi di questa tipologia.