A resolution based description logic calculus

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 easie...

Full description

Saved in:
Bibliographic Details
Main Author: Zombori Zsolt
Corporate Author: Symposium of Young Scientists on Intelligent Systems (3.) (2008) (Budapest)
Format: Article
Published: 2010
Series:Acta cybernetica 19 No. 3
Kulcsszavak:Számítástechnika, Kibernetika
Subjects:
Online Access:http://acta.bibl.u-szeged.hu/12881
Description
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 th e ALCHQ tableau method without requiring any further background knowledge.
Physical Description:571-590
ISSN:0324-721X