zbMATH — the first resource for mathematics

System description: E-KRhyper 1.4. Extensions for unique names and description logic. (English) Zbl 1381.68258
Bonacina, Maria Paola (ed.), Automated deduction – CADE-24. 24th international conference on automated deduction, Lake Placid, NY, USA, June 9–14, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38573-5/pbk). Lecture Notes in Computer Science 7898. Lecture Notes in Artificial Intelligence, 126-134 (2013).
Summary: 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 \(\mathcal{SHIQ}\) 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 \(\mathcal{SHIQ}\). 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.
For the entire collection see [Zbl 1264.68002].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T27 Logic in artificial intelligence
68T30 Knowledge representation
PDF BibTeX Cite
Full Text: DOI