=Paper=
{{Paper
|id=Vol-2013/paper6
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-2013/paper6.pdf
|volume=Vol-2013
}}
==None==
https://ceur-ws.org/Vol-2013/paper6.pdf
11
Automated Forgetting and Uniform
Interpolation: Three Tools
(Abstract of Invited Talk)
Renate A. Schmidt
School of Computer Science, The University of Manchester, UK
Forgetting eliminates symbols from a knowledge base so that consequences over
the remaining symbols in the signature are preserved. In logic the problem has
been studied as the uniform interpolation problem. Uniform interpolation is a
notion related to the Craig interpolation problem, but is stronger.
In computer science the importance of forgetting can be found in the knowl-
edge representation literature, specification refinement literature and the area of
description logic-based ontology engineering. In ontology-based information pro-
cessing, forgetting allows users to focus on specific parts of ontologies in order to
create decompositions and restricted views for in depth analysis or sharing with
other users. Forgetting is also useful for information hiding, explanation genera-
tion, semantic difference computation and ontology debugging. Forgetting is an
inherently difficult problem, much harder than standard reasoning (satisfiability
and validity testing), and very few logics are known to be complete for forgetting
(or have the uniform interpolation property). These not so encouraging premises
should however not prevent us from developing practical methods for computing
forgetting solutions and uniform interpolants.
My presentation gives an overview of the methods and success stories of three
forgetting tools:
– Scan, which performs second-order quantifier elimination [1, 2],
– Lethe, which solves the uniform interpolation problem for many expressive
description problems extending ALC [3, 4], and
– Fame, which computes semantic forgetting solutions for description logics
of different expressivity [5, 6].
References
1. D. M. Gabbay and H. J. Ohlbach. Quantifier elimination in second-order predicate
logic. South African Computer Journal, 7:35–43, 1992. Also published in B. Nebel,
C. Rich, W. R. Swartout, editors, Proceedings of the Third International Conference
on Principles of Knowledge Representation and Reasoning (KR’92), pages 425–436.
Morgan Kaufmann, 1992.
2. D. M. Gabbay, R. A. Schmidt, and A. Szalas. Second-Order Quantifier Elimina-
tion: Foundations, Computational Aspects and Applications, volume 12 of Studies
in Logic: Mathematical Logic and Foundations. College Publications, 2008.
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.
12
3. P. Koopmann and R. A. Schmidt. Uniform interpolation of ALC-ontologies using
fixpoints. In P. Fontaine, C. Ringeissen, and R. A. Schmidt, editors, Proceedings of
the 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013),
volume 8152 of Lecture Notes in Artificial Intelligence, pages 87–102. Springer, 2013.
4. P. Koopmann and R. A. Schmidt. Count and forget: Uniform interpolation of
SHQ-ontologies. In S. Demri, D. Kapur, and C. Weidenbach, editors, Automated
Reasoning (IJCAR 2014), volume 8562 of Lecture Notes in Artificial Intelligence,
pages 434–448. Springer, 2014.
5. Y. Zhao and R. A. Schmidt. Forgetting concept and role symbols in
ALCOIHµ+ (∇, u)-ontologies. In S. Kambhampati, editor, Proceedings of the
Twenty-Fifth International Joint Conference on Artificial Intelligence (IJCAI’16),
pages 1345–1352. AAAI Press/IJCAI, 2016.
6. Y. Zhao and R. A. Schmidt. Role forgetting for ALCOQH(∇)-ontologies using an
Ackermann approach. In C. Sierra, editor, Proceedings of the Twenty-Sixth Inter-
national Joint Conference on Artificial Intelligence (IJCAI’17), pages 1354–1361.
AAAI Press/IJCAI, 2017.