2013/11/12 by Viorica Sofronie-Stokkermans, Sofronie-Stokkermans, Viorica
Computer Science · #Algorithms and Data Compression #F.4.1 #FOS: Computer and information sciences #I.2.4 #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Numerical Methods and Algorithms
paper · pdf · doi:10.48550/arxiv.1311.2973
openalex publication_date 2013/11/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
In this paper we show that subsumption problems in lightweight description logics (such as EL and EL+) 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 EL, EL+ and extensions thereof. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend EL and EL+ with n-ary roles and/or numerical domains. As a by-product, this allows us to show that the algebraic models of \cal EL and \cal EL+ have ground interpolation and thus that \cal EL, \cal EL+, and their extensions studied in this paper have interpolation. We also show how these ideas can be used for the description logic EL++.