Representation Theorems and Locality for Subsumption Testing and Interpolation in the Description Logics ɛℒ, ɛℒ⁺ and their Extensions with n-ary Roles and Numerical Domains

Issue title: Helena Rasiowa’s Heritage in Mathematical Logic. Centenary Special Issue

Guest editors: Damian Niwiński and Ewa Orłowska

Article type: Research Article

Authors: Sofronie-Stokkermans, Viorica^{; *}

Affiliations: University Koblenz-Landau, Universitätsstraße 1, 56070 Koblenz, Germany. sofronie@uni-koblenz.de

Correspondence: [*] Address for correspondence: University Koblenz-Landau, Universitätsstraße 1, 56070 Koblenz, Germany

Abstract: In this paper we show that subsumption problems in lightweight description logics (such as ɛℒ and ɛℒ+) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras, to obtain uniform PTIME decision procedures for CBox subsumption in ɛℒ, ɛℒ+ and extensions thereof. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend ɛℒ and ɛℒ+ with n-ary roles and/or numerical domains. As a by-product, this allows us to show that the algebraic models of ɛℒ and ɛℒ+ have ground interpolation and thus that ɛℒ, ɛℒ+, and their extensions studied in this paper have interpolation.

DOI: 10.3233/FI-2017-1612

Journal: Fundamenta Informaticae, vol. 156, no. 3-4, pp. 361-411, 2017