Uniform interpolation of ALC-ontologies using fixpoints

Patrick Koopmann; Renate A. Schmidt

doi:10.1007/978-3-642-40885-4_7

Uniform interpolation of ALC-ontologies using fixpoints

Patrick Koopmann, Renate A. Schmidt

Formal Methods

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

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 ALCμ, which is ALC enriched with fixpoint operators, and always computes a finite representation. If the result does not involve fixpoint operators, it is the uniform interpolant in ALC. 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. © 2013 Springer-Verlag.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	87-102
Number of pages	15
Volume	8152
ISBN (Print)	9783642408847
DOIs	https://doi.org/10.1007/978-3-642-40885-4_7
Publication status	Published - 2013
Event	9th International Symposium on Frontiers of Combining Systems, FroCoS 2013 - Nancy Duration: 1 Jul 2013 → … http://www.cs.man.ac.uk/ schmidt/publications/KoopmannSchmidt13a.html

Publication series

Name	Lecture Notes in Artificial Intelligence

Conference

Conference	9th International Symposium on Frontiers of Combining Systems, FroCoS 2013
City	Nancy
Period	1/07/13 → …
Internet address	http://www.cs.man.ac.uk/ schmidt/publications/KoopmannSchmidt13a.html

Access to Document

10.1007/978-3-642-40885-4_7

Cite this

Koopmann, P., & Schmidt, R. A. (2013). Uniform interpolation of ALC-ontologies using fixpoints. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci. (Vol. 8152, pp. 87-102). (Lecture Notes in Artificial Intelligence). Springer Nature. https://doi.org/10.1007/978-3-642-40885-4_7

@inproceedings{3210aa5f281c4a918fab862e39f7759e,

title = "Uniform interpolation of ALC-ontologies using fixpoints",

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 ALCμ, which is ALC enriched with fixpoint operators, and always computes a finite representation. If the result does not involve fixpoint operators, it is the uniform interpolant in ALC. 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. {\textcopyright} 2013 Springer-Verlag.",

author = "Patrick Koopmann and Schmidt, {Renate A.}",

year = "2013",

doi = "10.1007/978-3-642-40885-4_7",

language = "English",

isbn = "9783642408847",

volume = "8152",

series = "Lecture Notes in Artificial Intelligence",

publisher = "Springer Nature",

pages = "87--102",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

address = "United States",

note = "9th International Symposium on Frontiers of Combining Systems, FroCoS 2013 ; Conference date: 01-07-2013",

url = "http://www.cs.man.ac.uk/ schmidt/publications/KoopmannSchmidt13a.html",

}

Koopmann, P & Schmidt, RA 2013, Uniform interpolation of ALC-ontologies using fixpoints. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 8152, Lecture Notes in Artificial Intelligence, Springer Nature, pp. 87-102, 9th International Symposium on Frontiers of Combining Systems, FroCoS 2013, Nancy, 1/07/13. https://doi.org/10.1007/978-3-642-40885-4_7

Uniform interpolation of ALC-ontologies using fixpoints. / Koopmann, Patrick; Schmidt, Renate A.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 8152 Springer Nature, 2013. p. 87-102 (Lecture Notes in Artificial Intelligence).

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Uniform interpolation of ALC-ontologies using fixpoints

AU - Koopmann, Patrick

AU - Schmidt, Renate A.

PY - 2013

Y1 - 2013

N2 - 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 ALCμ, which is ALC enriched with fixpoint operators, and always computes a finite representation. If the result does not involve fixpoint operators, it is the uniform interpolant in ALC. 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. © 2013 Springer-Verlag.

AB - 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 ALCμ, which is ALC enriched with fixpoint operators, and always computes a finite representation. If the result does not involve fixpoint operators, it is the uniform interpolant in ALC. 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. © 2013 Springer-Verlag.

U2 - 10.1007/978-3-642-40885-4_7

DO - 10.1007/978-3-642-40885-4_7

M3 - Conference contribution

SN - 9783642408847

VL - 8152

T3 - Lecture Notes in Artificial Intelligence

SP - 87

EP - 102

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 9th International Symposium on Frontiers of Combining Systems, FroCoS 2013

Y2 - 1 July 2013

ER -

Uniform interpolation of ALC-ontologies using fixpoints

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this