TY - GEN
T1 - On the complexity of finding good proofs for description logic entailments
AU - Alrabbaa, Christian
AU - Baader, Franz
AU - Borgwardt, Stefan
AU - Koopmann, Patrick
AU - Kovtunova, Alisa
PY - 2020
Y1 - 2020
N2 - If a Description Logic (DL) system derives a consequence, then one can in principle explain such an entailment by presenting a proof of the consequence in an appropriate calculus. Intuitively, good proofs are ones that are simple enough to be comprehensible to a user of the system. In recent work, we have introduced a general framework in which proofs are represented as labeled, directed hypergraphs, and have investigated the complexity of finding small proofs. However, large size is not the only reason that can make a proof complex. In the present paper, we introduce other measures for the complexity of a proof, and analyze the computational complexity of deciding whether a given consequence has a proof of complexity at most q. This problem can be NP-complete even for EL, but we also identify measures where it can be decided in polynomial time.
AB - If a Description Logic (DL) system derives a consequence, then one can in principle explain such an entailment by presenting a proof of the consequence in an appropriate calculus. Intuitively, good proofs are ones that are simple enough to be comprehensible to a user of the system. In recent work, we have introduced a general framework in which proofs are represented as labeled, directed hypergraphs, and have investigated the complexity of finding small proofs. However, large size is not the only reason that can make a proof complex. In the present paper, we introduce other measures for the complexity of a proof, and analyze the computational complexity of deciding whether a given consequence has a proof of complexity at most q. This problem can be NP-complete even for EL, but we also identify measures where it can be decided in polynomial time.
UR - http://www.scopus.com/inward/record.url?scp=85091423373&partnerID=8YFLogxK
M3 - Conference contribution
VL - 2663
T3 - CEUR Workshop Proceedings
BT - DL 2020 - Proceedings of the 33rd International Workshop on Description Logics, co-located with the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020
A2 - Borgwardt, S.
A2 - Meyer, T.
PB - CEUR-WS
T2 - 33rd International Workshop on Description Logics, DL 2020
Y2 - 12 September 2020 through 14 September 2020
ER -