Description logics are a family of logics that provide formalisms for representing and reasoning about knowledge, based on describing concepts, in a structured and formally well-understood way. They provide the logical foundation for the web ontology language (OWL), which increased awareness of them recently. The most popular techniques for decision procedures for description logics are tableau reasoning methods, which have a long tradition and are well established in automated reasoning. This thesis investigates the possibility of finding a general and optimised blocking mechanism for description logics with the finite model property. It suggests that, while the high branching factor for unrestricted blocking reduces its performance, suitable control of the application of the blocking rule can make the performance acceptable while preserving termination. This claim is supported by experiments that compare the performance of two sample controlled versions of unrestricted blocking. In order to show the generality and power of controlled versions of unrestricted blocking, it is shown how some of the mainstream and most successful standard blocking mechanisms can be approximated as restricted forms of unrestricted blocking. These approximations have the advantage of always being sound compared to their standard versions, which are known to be sound only for some logics. Here, a variation of unrestricted blocking which can ensure strong termination is also introduced. This is done through introducing a new rule that uses the inequality expressions introduced by the blocking rule. The weak termination property of unrestricted blocking is one of its weak points which by this variant of blocking can be addressed. The work presented in this thesis should be of value to people who are working on generalising different aspects of reasoning methods. As blocking plays a critical role in termination of tableau provers, exploration of different variations of unrestricted blocking introduced here may be also of interest for the artificial intelligence researcher.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:674706 |
| Date | January 2015 |
| Creators | Khodadadi, Mohammad |
| 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/exploration-of-variations-of-unrestricted-blocking-for-description-logics(3fc15638-1483-42d0-a827-75cb231f0737).html |
Page generated in 0.0022 seconds