Abstract
We present a method to compute uniform interpolants with fixpoints for ontologies specified in the description logic ALC. The aim of uniform interpolation is to reformulate an ontology such that it only uses a specified set of symbols, while preserving consequences that involve these symbols. It is known that in ALC uniform interpolants cannot always be finitely represented. Our method computes uniform interpolants for the target language ALCmu, which is ALC enriched with fixpoint operators, and always computes a finite representation. The method focuses on eliminating concept symbols and combines resolution-based reasoning with an approach known from the area of second-order quantifier elimination to introduce fixpoint operators when needed. If fixpoint operators are not desired, it is possible to approximate the interpolant.
| Original language | English |
|---|---|
| Title of host publication | Frontiers of Combining Systems |
| Editors | Pascal Fontaine, Christophe Ringeissen, Renate A Schmidt |
| Publisher | Springer Nature |
| Pages | 87-102 |
| Number of pages | 16 |
| Publication status | Published - 2013 |
| Event | Frontiers of Combining Systems 2013 - Nancy, France Duration: 18 Sept 2013 → 20 Sept 2013 |
Conference
| Conference | Frontiers of Combining Systems 2013 |
|---|---|
| City | Nancy, France |
| Period | 18/09/13 → 20/09/13 |
Keywords
- description logics
- uniform interpolation
- forgetting
- fixpoints