 |
    |
System Description: E-KRHyper 1.4
Extensions for Unique Names and Description Logic
Markus Bender, Björn Pelzer, and Claudia Schon
Universität Koblenz-Landau, Institut für Informatik, 56070, Koblenz, Germanybpelzer@uni-koblenz.de
schon@uni-koblenz.de
Abstract. Formal ontologies may go beyond first-order logic (FOL) in their expressivity, hindering the usage of common automated theorem provers (ATP) for ontology reasoning. The Unique Name Assumption (UNA) is an extension to FOL that is valuable for ontology specification, allowing the definition of distinct objects. Likewise, the Description Logic 
is a popular language for knowledge representation (KR). This system description provides details on the extension of the prover E-KRHyper by the ability to handle both the UNA and 
. This ATP was developed for embedding in KR applications and hence already equipped with special features and extensions to FOL, making it natural to add the new capabilities in E-KRHyper version 1.4. We report on the theory, the implementation and also the evaluation results of the new features.
LNAI 7898, p. 126 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2013