Logiche Descrittive e ragionamento non monotono. Si sono definite logiche descrittive preferenziali introducendo una nozione di "tipicalità" nel linguaggio allo scopo di  modellare proprietà prototipali dei concetti di un'ontologia in OWL e di catturare l'ereditarietà con eccezioni.  Per quanto riguarda i meccanismi di ragionamento si sono utilizzati metodi di prova basati sui tableaux e costruzioni quali la Rational Closure, utilizzando codifiche delle logiche preferenziali nelle logiche standard. Sono state inoltre studiate logiche descrittive defeasible basate su semantiche multi-preferenziali che raffinano la rational closure, nonché semantiche multi-preferenziali concept-wise per  ranked e weighted  knowledge bases. Le logiche descrittive multi-preferenziali (a due valori e fuzzy) sono state utilizzate nel definire una semantica logica per alcuni modelli di reti neurali, quali le Self-Organising Maps ed i Multilayer Perceptrons. Per ragionare nelle logiche descrittive defeasible a bassa complessità sono stati svilippati metodi di prova basati sull'Answer Set Programming (ASP).

Model checking in ASP. Si è definita un’estensione temporale di ASP per ragionare sull’esecuzione di azioni complesse e computazioni infinite, sviluppando tecniche di Bounded Model Checking in ASP per la verifica di proprietà temporali di un dominio.

Verifica di conformità di processi di business. Questa attività è iniziata nel progetto della Regione Piemonte "ICT4LAW: ICT Converging on Law: Next Generation Services for Citizens, Enterprises, Public Administration and Policymakers” (2009-2013) in cui si è affrontato il problema di verificare la conformità (compliance) dei processi di business alle norme. Partendo dai processi di business specificati in YAWL, si utilizzato ASP con constraints per modellare i dati e l'astrazione sui dati nella verifica dei processi.  Inoltre, è stato sviluppato un approccio per rappresentare le principali tipologie di obblighi utilizzate nella verifica di conformità dei processi in una logica tempoirale deontica linear-time. Recentemente si è definita una estensione preferenziale (con tipicalità) della logica temporale deontica

-------------------------------------------------------------------------------

Description Logics and  Non Monotonic Reasoning. We have developed preferential description logics with typicality. The typicality construct is used to model prototypical properties of concepts in an OWL ontology and to capture inheritance with exceptions. Proof methods have been developed through tableau, through the Rational Closure construction and other constructions, exploiting encoding of the preferential DLs into standard DLs, as well as through translation in ASP. Defeasible description logics, based on multi-preferential semantics, have also been studied, by developing refinements of the rational closure, as well as concept-wise multipreference semantics for ranked knowledge bases and for weighted knowledge bases.  Two valued and fuzzy multi-preferential description logics have been exploited to provide a logical semantics for some neural network models, namely, Self-Organising Maps and Multilayer Perceptrons. Proof methods based on Answer Set Programming (ASP) encodings have been developed for defeasible reasoning in preferential and multi-preferential lightweight description logics.

Model checking in ASP. A temporal extension of ASP has been defined for reasoning in action theories with complex actions and infinite computations. Bounded Model Checking techniques have been developed in ASP for the verification of temporal properties of actions domains.

Business processes  compliance verification. This activity  was part of the project of the  Regione Piemonte "ICT4LAW: ICT Converging on Law: Next Generation Services for Citizens, Enterprises, Public Administration and Policymakers” (2009-2013). The problem of compliance of business processes to norms has been addressed using ASP with constraints to model data aware processes and data abstraction in process verification. Different kinds of obligations have been considered in a Deontic extension of Linear Time Temporal Logic., which are useful in the verification of compliance to normative requirements. Recent work deals with conditional/preferential  extensions of  such a temporal deontic logic.