=Paper=
{{Paper
|id=Vol-2013/paper10
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2013/paper10.pdf
|volume=Vol-2013
}}
==None==
https://ceur-ws.org/Vol-2013/paper10.pdf
17
Resolution Based Uniform Interpolation and
Forgetting for Expressive Description Logics
(Abstract of Tutorial)
Patrick Koopmann
Institute of Theoretical Comp. Science, Technische Universität Dresden, Germany
patrick.koopmann@tu-dresden.de
This tutorial discusses resolution-based methods for computing uniform inter-
polants in various expressive description logics (DLs) and their implementations,
and their relations to second-order quantifier elimination. DLs [1] are fragments
of first-order logic used to define terminological knowledge in form of ontolo-
gies, using a set of unary and binary predicates called concept and role names,
which form the signature of the ontology. Forgetting a set of given concept and
role names from an ontology means computing a new ontology that does not
use these concept and role names, but preserves all logical entailments of the
original ontology over the remaining signature. The resulting ontology is then a
uniform interpolant of the original ontology for the remaining signature. There
is a range of applications for uniform interpolants, such as for ontology reuse,
ontology analysis, or computing logical differences.
Theoretical results on uniform interpolation seem discouraging. In most known
DLs, uniform interpolants do not always exist, and already the problem of de-
ciding whether a uniform interpolant exists for a given ontology and signature
is ExpTime-complete for the Horn DL EL [7], and 2ExpTime-complete for the
expressive DL ALC [8]. Moreover, in both DLs, uniform interpolants have in the
worst case a size that is triple-exponential in the size of the input ontology [9,8].
The former problem can be solved by computing uniform interpolants in DLs
that have fixpoint operators, which often ensures that uniform interpolants do
always exist. Regarding the size of the uniform interpolants, experiments indi-
cate that the worst-case rarely occurs with real-life ontologies, and that uniform
interpolants are in most cases not larger than the original ontology. However,
due to the high worst case complexity, the practical computation of uniform
interpolants in expressive DLs requires dedicated and goal-oriented procedures.
Forgetting and uniform interpolation are similar to second-order quantifier
elimination in the sense that the goal is to eliminate predicates from a logical for-
mulae, while preserving logical entailments in the remaining signature. However,
while the result of second-order quantifier preserves all second-order entailments
of the original formula, uniform interpolants only preserve entailments that can
be expressed in the DL at hand. Despite these differences, the similarity to
second-order quantifier elimination motivates the use of similar techniques for
computing uniform interpolants. This tutorial presents such an approach, which
is based on the idea of computing relevant entailments using resolution. For this,
it uses a resolution-based calculus that was first presented in [2] for the DL ALC,
and later extended to more expressive DLs such as SHQ [3] and SIF [5], as
Copyright c 2017 by the paper’s authors
In: P. Koopmann, S. Rudolph, R. Schmidt, C. Wernhard (eds.): SOQE 2017 – Pro-
ceedings of the Workshop on Second-Order Quantifier Elimination and Related Topics,
Dresden, Germany, December 6–8, 2017, published at http://ceur-ws.org.
18
well as to knowledge bases with ABoxes [6]. In theory, these calculi can be seen
as a consequence-based reasoning procedures that could also be used for clas-
sical reasoning tasks such as consistency-checking or classification. However, in
order to be suited for computing uniform interpolants, they have to satisfy ad-
ditional completeness conditions tailored towards the computation of uniform
interpolants. We will present some of these calculi, and discuss algorithms and
optimisations used in the tool Lethe [4] for computing uniform interpolants.
References
1. Baader, F., Calvanese, D., McGuinness, D.L., Nardi, D., Patel-Schneider, P.F.
(eds.): The Description Logic Handbook: Theory, Implementation, and Applica-
tions. Cambridge University Press (2003)
2. Koopmann, P., Schmidt, R.A.: Uniform interpolation of ALC-ontologies using fix-
points. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) Frontiers of Combining
Systems: 9th International Symposium, FroCoS 2013, Nancy, France, September 18-
20, 2013. Proceedings. pp. 87–102. Springer Berlin Heidelberg, Berlin, Heidelberg
(2013), https://doi.org/10.1007/978-3-642-40885-4_7
3. Koopmann, P., Schmidt, R.A.: Count and forget: Uniform interpolation of SHQ-
ontologies. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning:
7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Sum-
mer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings. Springer
International Publishing, Cham (2014)
4. Koopmann, P., Schmidt, R.A.: Lethe: Saturation-based reasoning for non-standard
reasoning tasks. In: Informal Proceedings of the 4th International Workshop on
OWL Reasoner Evaluation (ORE-2015) co-located with the 28th International
Workshop on Description Logics (DL 2015), Athens, Greece, June 6, 2015. pp. 23–30
(2015), http://ceur-ws.org/Vol-1387/paper_9.pdf
5. Koopmann, P., Schmidt, R.A.: Saturated-based forgetting in the description
logic SIF. In: Proceedings of the 28th International Workshop on Description
Logics, Athens,Greece, June 7-10, 2015. (2015), http://ceur-ws.org/Vol-1350/
paper-53.pdf
6. Koopmann, P., Schmidt, R.A.: Uniform interpolation and forgetting for ALC on-
tologies with ABoxes. In: Proceedings of the Twenty-Ninth AAAI Conference on
Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA. pp. 175–181 (2015),
http://www.aaai.org/ocs/index.php/AAAI/AAAI15/paper/view/9981
7. Lutz, C., Seylan, I., Wolter, F.: An automata-theoretic approach to uniform inter-
polation and approximation in the description logic EL. In: Principles of Knowledge
Representation and Reasoning: Proceedings of the Thirteenth International Confer-
ence, KR 2012, Rome, Italy, June 10-14, 2012 (2012), http://www.aaai.org/ocs/
index.php/KR/KR12/paper/view/4511
8. Lutz, C., Wolter, F.: Foundations for uniform interpolation and forgetting in expres-
sive description logics. In: IJCAI 2011, Proceedings of the 22nd International Joint
Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011.
pp. 989–995 (2011), https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-170
9. Nikitina, N., Rudolph, S.: (Non-)succinctness of uniform interpolants of general
terminologies in the description logic EL. Artif. Intell. 215, 120–140 (2014), https:
//doi.org/10.1016/j.artint.2014.06.005