Logiche Descrittive e ragionamento non monotono. Questa attività si è svolta nell’ambito dei progetti: INDAM - GNCS 2015 "Logiche Descrittive e Ragionamento Non Monotono", INDAM - GNCS 2016 "Ragionamento Defeasible nelle Logiche Descrittive”, INDAM - GNCS 2018-2020 e nel progetto PRIN 2008  "Logiche Descrittive Nonmonotone: Complessità e implementazioni (LoDeN)". Si sono definite logiche descrittive preferenziali introducendo una nozione di "tipicalità" 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 e  semantiche multi-preferenziali concept-wise per  ranked 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.

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

Description Logics and  Non Monotonic Reasoning. This activity  has been part of the projects: INDAM - GNCS 2015 "Description Logics and  Non Monotonic Reasoning", INDAM - GNCS 2016 "Defeasible Reasoning in Description Logics”, INDAM - GNCS 2018 - 2020,  and of the project PRIN 2008 :" Nonmonotonic Description Logics: Complexity and implementations (LoDeN)".  Preferential description logics have been developed, defining a notion of typicality, to model prototypical properties of concepts in an OWL ontology and to capture inheritance with exceptions. Proof methods have been developed through tableaux, through the Rational Closure construction, 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.  Two valued and fuzzy multi-preferential description logics have been exploited to define 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, useful in the verification of compliance to normative requirements.