Oscar Barreca

Description logic (DL) knowledge bases (KBs) built by hand or (semi)automatically using machine learning or information retrieval tools may contain errors, often detected when reasoning derives an inconsistency. However, not all errors cause an inconsistency. Such errors may be noticed when reasoning produces a consequence that follows from the KB, but does not hold in the application domain modelled by the KB. In fact, some applicationrelevant DL KBs such as the large medical ontology SNOMED CT are written in DL dialects, like \(EL\), that cannot even express inconsistencies. Eliminating an inconsistency or an unwanted consequence by removing a minimal amount of information from the KB is usually called repair in the DL literature. Instead of producing a single new KB as a repair, inconsistency-tolerant reasoning takes all repairs of a detected inconsistency into account, e.g., by producing consequences that follow from all repairs or from some repair. This notion can be extended to repairs that remove an unwanted consequence, in which case it is called error-tolerant reasoning. This paper shows in an exemplary way how results for inconsistency-tolerant reasoning can be transferred to error-tolerant reasoning. To this purpose, it generalizes an existing approach connecting inconsistency-tolerant reasoning over prioritized DL-Lite KBs and argumentation frameworks to the setting of error-tolerant reasoning for \(EL\) KBs.

@inproceedings{ BaaderErrors2026,
  author = {Franz {Baader} and Oscar {Barreca}},
  booktitle = {Logical {{Approaches}} to {{Handling Inconsistent Data}} ({{LINDA}})},
  title = {Errors {{Need Not Show Up}} as {{Inconsistencies}}: {{From Error-tolerant Reasoning}} to {{Argumentation Frameworks}}},
  venue = {Lisbon},
  year = {2026},
}

Given an interpretation \(I\) and a formula \(\varphi\) written in a logic \(L\), the problem of model checking (MC) for \(L\) is the problem of determining whether \(I\) is a model of \(\varphi\). In this work, the computational complexity of MC for temporal equilibrium logic (TEL), a temporal extension of ASP, is investigated. The complexity of the universal and the existential variant of MC for TEL over Kripke structures, and of MC over linear traces, is determined. The complexity of these problems when the set of temporal operators, the temporal height or the implication height of the input formula is restricted is also determined.

@inproceedings{ BarrecaComplexity2026,
  author = {Oscar {Barreca} and Thomas {Eiter} and Davide {Sold\`a}},
  booktitle = {Logic {{Programming}} and {{Nonmonotonic Reasoning}}},
  note = {To appear.},
  publisher = {Springer},
  title = {On the {{Complexity}} of {{Model Checking}} for {{Temporal Equilibrium Logic}}},
  venue = {Klagenfurt},
  year = {2026},
}