The problem of optimising automated explanations for entailments in knowledge bases is tackled by modelling deductive reasoning processes using the cognitive architecture ACT-R. This results in the model SHARP which simulates a tableau algorithm for deciding inconsistency of an ABox in the description logic 𝒜ℒℰ as executed by a human. SHARP enables predicting the inference time of this task, which is assumed to reflect human performance. With the inference time, two complexity measures on ABoxes are defined that cognitively adequate by design.

Opponent: Jakub Szymanik, Associate professor in the Center for Brain/Mind Sciences and the Computer Science Department at the University of Trento.