Campus Event Calendar
Event Entry
What and Who
Computing Uniform Interpolation for Description Logics
Renate Schmidt
University of Manchester
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI
Public Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 4 December 2013
14:15
60 Minutes
E1 5
002
Saarbrücken
Abstract
This is joint work with Patrick Koopmann. We consider the problem of
computing uniform interpolants for ontologies specified in the
description logics ALC and ALCH. Uniform interpolation aims to minimally
characterise a given ontology relative to a sublanguage of specified
symbols, in such a way that consequences involving these symbols are
preserved. Though existence of uniform interpolants is decidable it is
known that in ALC uniform interpolants cannot always be finitely
represented. Our method computes uniform interpolants for ALC with
fixpoint operators and always computes a finite representation. The
method can eliminate both concept and role symbols and combines
resolution-based reasoning with ideas 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
uniform interpolant. Experiments on ALC and ALCH fragments of from
a large corpus of ontologies from real-world applications show that our
method is practical and widely applicable.
computing uniform interpolants for ontologies specified in the
description logics ALC and ALCH. Uniform interpolation aims to minimally
characterise a given ontology relative to a sublanguage of specified
symbols, in such a way that consequences involving these symbols are
preserved. Though existence of uniform interpolants is decidable it is
known that in ALC uniform interpolants cannot always be finitely
represented. Our method computes uniform interpolants for ALC with
fixpoint operators and always computes a finite representation. The
method can eliminate both concept and role symbols and combines
resolution-based reasoning with ideas 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
uniform interpolant. Experiments on ALC and ALCH fragments of from
a large corpus of ontologies from real-world applications show that our
method is practical and widely applicable.
Contact
Jennifer Müller
2900
--email hidden
passcode not visible
logged in users only
Jennifer Müller, 11/29/2013 14:26 -- Created document.