Count and Forget: Uniform Interpolation of SHQ-Ontologies.

Koopmann, P. and Schmidt, R. A. (2014)

In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 434-448. BiBTeX, Long version (final version available via DOI link to Springer).

We propose a method for forgetting concept and non-transitive roles symbols of SHQ-ontologies, or for computing uniform interpolants in SHQ. A uniform interpolant of an ontology over a specified set of symbols is a new ontology that only uses the specified symbols, and preserves all logical entailments that can be expressed in SHQ using these symbols. Uniform interpolation has applications in ontology reuse, information hiding and ontology analysis, but so far no method for computing uniform interpolants for expressive description logics with number restrictions has been developed. Our results are not only interesting because they allow to compute uniform interpolants of ontologies that are in a more expressive language. Using number restrictions also allows to preserve more information in uniform interpolants of ontologies in less complex logics, such as ALC or EL. The presented method computes uniform interpolants on the basis of a new resolution calculus for SHQ-ontologies, that allows to derive consequences in a goal-oriented manner. The output of our method is expressed using SHQmu, which is SHQ extended with fixpoint operators, to always enable a finite representation of the uniform interpolant.

Long version.


Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 21 Jun 15
Copyright © 2014 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk