Explanation through cut elimination

Abstract

Il presente lavoro affronta il "problema della spiegazione" nell'ambito dell'ingegneria ontologica, concentrandosi sui sistemi basati sulle logiche descrittive. I ragionatori basati su tableau, pur essendo molto efficienti, applicano profonde trasformazioni sintattiche che rendono i loro processi inferenziali difficilmente comprensibili per gli utenti umani. Per risolvere questa criticità, la tesi propone di utilizzare il calcolo dei sequenti come framework formale per generare spiegazioni concettuali chiare e intuitive. Viene definito un quadro operativo che pone come requisito fondamentale la riduzione della complessità concettuale dall'explanandum all'explanans. Lo studio analizza inizialmente il sistema HALC originariamente proposto da Borgida et al., per poi introdurre un calcolo dei sequenti etichettato in stile G3, denominato G3ALC*, capace di estendere la formulazione delle spiegazioni a linguaggi ontologici più espressivi come SROIQ. Il contributo centrale del lavoro consiste nel dimostrare la validità del teorema di eliminazione del taglio per entrambi i calcoli presentati. Tale risultato strutturale garantisce la proprietà della sottoformula, la quale assicura formalmente la progressiva riduzione della complessità concettuale necessaria per produrre spiegazioni umane autentiche e comprensibili.

This work addresses the “explanation problem” within the field of ontology engineering, focusing on Description Logics (DLs) systems. While highly efficient, tableau-based reasoners apply deep syntactic transformations that make their inferential processes difficult for human users to intuitively understand. To address this problem, we propose using sequent calculus as a formal framework to generate clear and accessible conceptual explanations. To achieve that, we define an operational framework, positing the reduction of conceptual complexity from the explanandum to the explanans as a fundamental requirement of genuine explanations. The study initially analyzes the HALC system originally proposed by Borgida et al. to address the same problem. Subsequently, it introduces a G3-style labelled sequent calculus, denoted as G3ALC*, capable of extending the formulation of explanations to more expressive ontological languages such as SROIQ. The central contribution of the work consists of proving the cut-elimination theorem for both presented calculi. This structural result guarantees the subformula property, which formally ensures the progressive reduction of conceptual complexity necessary to produce genuine and comprehensible human explanations.