Design of optimization techniques and software architectures for description logic reasoners

提出的研究计划主要涉及描述逻辑（DL）推理器优化技术的设计和经验评估。在过去的十年中，深度学习推理已经获得了语义web社区的相当多的关注，因为web本体语言OWL及其后续OWL 2是基于描述逻辑的。owl2的深度学习子集是一个众所周知的、表达能力很强的深度学习的语法变体。粗略地说，深度学习知识是用概念、角色和个体来描述的，这些概念、角色和个体可以与各种构造器组合在一起。概念描述具有共同属性的个体集合，角色指定个体之间的二元关系。owl2 DL的概念可满足性问题已知为2- nexptime -complete。大多数推理都是基于表格（证明）程序。由于演算的结构和推理问题固有的时间复杂性，这些演算的实现需要高度复杂的优化技术。需要大量的表优化技术来加速提供的推理服务，使深度学习推理在实际应用中可行。**我们建议继续对深度学习推理器的优化技术和软件架构的设计进行研究，即使需要不可处理的推理，目标也是实现更好的可扩展性。主要的预期结果是(i)新颖的代数表方法和相应的优化技术，解决了OWL 2dl语言特征（如合格基数限制、标称和逆角色）组合的标准表方法中已知的低效问题；（ii）新的并行深度学习推理架构，将支持现代多处理器和多核硬件，并提供与可用核数量大致线性的速度改进。预期的结果对于语义web社区本体开发的持续成功非常重要，特别是因为本体的大小和复杂性经常以这样一种方式增加，（不可处理的）深度学习推理所需的时间已成为主要障碍。****

The proposed research program is mainly concerned with the design and empirical evaluation of optimization techniques for description logic (DL) reasoners. Over the last decade DL reasoning has gained quite some attention from the semantic web community because the Web Ontology Language, OWL, and its sequel OWL 2 are based on description logics. The DL subset of OWL 2 is a syntactic variant of a well-known and very expressive DL. Roughly speaking DL knowledge is described using concepts, roles, and individuals that can be combined with various constructors. Concepts describe sets of individuals with common properties and roles specify binary relationships between individuals. The concept satisfiability problem for OWL 2 DL is known to be 2-NExpTime-complete. Most reasoners are based on tableau (proof) procedures. The implementation of these calculi requires highly sophisticated optimization techniques due to the structure of the calculi and the inherent time complexity of the inference problems. A large set of tableau optimization techniques needs to be applied to speed up provided inference services and make DL reasoning feasible in practical applications.**We propose to continue with our research on the design of optimization techniques and software architectures for DL reasoners with the goal to achieve better scalability even if non-tractable reasoning is required. The major expected outcomes are (i) novel algebraic tableau methods and corresponding optimization techniques that resolve known inefficiencies in standard tableau methods for combinations of OWL 2 DL language features such as qualified cardinality restrictions, nominals, and inverse roles; (ii) new parallel DL reasoning architectures that will support modern multi-processor and multi-core hardware and offer speed improvements that are roughly linear to the number of available cores. The expected outcomes are important for the continued success of ontology development in the semantic web community, especially since the size and complexity of ontologies has often increased in such a way that the time required for (non-tractable) DL reasoning has become a major obstacle.****