The thesis investigates methods for uniform interpolation in expressive description logics. Description logics are formalisms commonly used to model ontologies. Ontologies store terminological information and are used in a wide range of applications, such as the semantic web, medicine, bio-informatics, software development, data bases and language processing. Uniform interpolation eliminates terms from an ontology such that logical entailments in the remaining language are preserved. The result, the uniform interpolant, is a restricted view of the ontology that can be used for a variety of tasks such as ontology analysis, ontology reuse, ontology evolution and information hiding. Uniform interpolation for description logics has only gained an interest in the research community in the last years, and theoretical results show that it is a hard problem requiring specialised reasoning approaches. We present a range of uniform interpolation methods that can deal with expressive description logics such as ALC and many of its extensions. For all these logics, these are the first methods that are able to compute uniform interpolants for all inputs. The methods are based a new family of saturation-based reasoning methods, which make it possible to eliminate symbols in a goal-oriented manner. The practicality of this approach is shown by an evaluation on realistic ontologies.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:674705 |
| Date | January 2015 |
| Creators | Koopmann, Patrick |
| Publisher | University of Manchester |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | https://www.research.manchester.ac.uk/portal/en/theses/practical-uniform-interpolation-for-expressive-description-logics(b04c6bc6-0877-488b-86d7-fa37ae99eeb6).html |
Page generated in 0.0017 seconds