Algorithmic Approaches for Inconsistency Measurement

Dealing with inconsistent information is an essential task within the field of artificial intelligence.  Inconsistency measurement offers a quantitative framework as a means to analyze and interpret such inconsistencies. To be precise, an inconsistency measure computes a numerical value which captures the level of inconsistency. The literature provides a wide range of inconsistency measures for different domains, such as databases, ontologies, and various logics. As inconsistency measurement is generally computationally hard, efficient algorithmic solutions are needed in order to facilitate the use of inconsistency measures in practical applications. Therefore, the overarching goal of this thesis is to develop, analyze, and evaluate algorithmic approaches for inconsistency measurement.

We consider a total of 8 inconsistency measures for propositional logic as well as 4 measures for linear temporal logic on fixed traces (LTLff). More precisely, these are the contension, forgetting-based, hitting set, max-distance, sum-distance, hit-distance, problematic, and MUS-variable-based measures for propositional logic, and the LTL time, LTL contension, LTL problematic, and LTL MUS-variable-based measures for LTLff. With regard to the 8 measures for propositional logic, the associated decision problems of 6 of them are complete for the first level of the polynomial hierarchy (namely, these are the contension, forgetting-based, hitting set, max-distance, sum-distance, and hit-distance measures), and the associated decision problems of the remaining 2 are complete for the second level (consequently, these are the problematic and the MUS-variable-based measures). Regarding LTLff, the corresponding decision problems of 2 inconsistency measures are complete for the first level (these are the LTL time and the LTL contension measure), and 2 are complete for the second level (these are the LTL problematic and the LTL MUS-variable-based measure).

With regard to the inconsistency measures that are associated with the first level of the polynomial hierarchy, we present algorithmic approaches based on answer set programming (ASP), Boolean satisfiability (SAT) solving, and maximum satisfiability (MaxSAT) solving. For the measures associated with the second level of the polynomial hierarchy, we apply ASP again, in addition to SAT-based counterexample-guided abstraction refinement (CEGAR). All approaches have been implemented and evaluated experimentally in order to compare the performance of the different solutions w.r.t. each measure. Thus, on the one hand, this thesis presents theoretical results in terms of ASP, SAT, and MaxSAT encodings and the respective correctness proofs, and on the other hand, it provides empirical results in the form of experimental evaluations.