Zsombori, Zsolt A resolution based description logic calculus. (English) Zbl 1224.68168 Acta Cybern. 19, No. 3, 571-590 (2010). Summary: We present a resolution based reasoning algorithm called DL calculus that decides concept satisfiability for the SHQ language. Unlike existing resolution based approaches, the DL calculus is defined directly on DL expressions. We argue that working on this high level of abstraction provides an easier to grasp algorithm with less intermediary transformation steps and increased efficiency. We give a proof of the completeness of our algorithm that relies solely on the ALCHQ tableau method, without requiring any further background knowledge. MSC: 68T35 Theory of languages and software systems (knowledge-based systems, expert systems, etc.) for artificial intelligence 68T27 Logic in artificial intelligence Keywords:DL calculus; SHQ language Software:DLog PDFBibTeX XMLCite \textit{Z. Zsombori}, Acta Cybern. 19, No. 3, 571--590 (2010; Zbl 1224.68168)