SROIQsigma is decidable

We consider a dynamic extension of the description logic \(\mathcal{SROIQ}\). This means that interpretations could evolve thanks to some actions such as addition and/or deletion of an element (respectively, a pair of elements) of a concept (respectively, of a role). The obtained logic is called \(\...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2014-11
Main Authors: Brenas, Jon Haël, Echahed, Rachid, Strecker, Martin
Format: Article
Language:English
Subjects:
Deletion
Substitutes
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We consider a dynamic extension of the description logic \(\mathcal{SROIQ}\). This means that interpretations could evolve thanks to some actions such as addition and/or deletion of an element (respectively, a pair of elements) of a concept (respectively, of a role). The obtained logic is called \(\mathcal{SROIQ}\) with explicit substitutions and is written \(\mathcal{SROIQ^\sigma}\). Substitution is not treated as meta-operation that is carried out immediately, but the operation of substitution may be delayed, so that sub-formulae of \(\mathcal{SROIQ}^\sigma\) are of the form \(\Phi\sigma\), where \(\Phi\) is a \(\mathcal{SROIQ}\) formula and \(\sigma\) is a substitution which encodes changes of concepts and roles. In this paper, we particularly prove that the satisfiability problem of \(\mathcal{SROIQ}^\sigma\) is decidable.
ISSN:2331-8422