KR2020Proceedings of the 17th International Conference on Principles of Knowledge Representation and ReasoningProceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning

Rhodes, Greece. September 12-18, 2020.

Edited by
  1. Diego Calvanese
  2. Esra Erdem
  3. Michael Thielscher

ISSN: 2334-1033
ISBN: 978-0-9992411-7-2

Sponsored by
Published by

Copyright © 2020 International Joint Conferences on Artificial Intelligence Organization

On the Decidability of Expressive Description Logics with Transitive Closure and Regular Role Expressions

  1. Jean Christoph Jung(University of Bremen)
  2. Carsten Lutz(University of Bremen)
  3. Thomas Zeume(Ruhr University Bochum)
PDF
BibTeX
DOI 10.24963/kr.2020/53

Keywords

  1. Computational aspects of knowledge representation-General
  2. Description logics-General

Abstract

We consider fragments of the description logic SHOIF extended with regular expressions on roles. Our main result is that satisfiability and finite satisfiability are decidable in two fragments SHOIF^1 and SHOIF^2, NExpTime-complete for the former and in 2NExpTime for the more expressive latter fragment. Both fragments impose restrictions on regular role expressions of the form r*. SHOIF^1 encompasses the extension of SHOIF with transitive closure of roles (when functional roles have no subroles) and the modal logic of linear orders and successor, with converse. Consequently, these logics are also decidable and NExpTime-complete.