Locality and Applications to Subsumption Testing in EL and Some of its Extensions

DOI10.7561/SACS.2013.2.251zbMATH Open1424.68157arXiv1311.2973MaRDI QIDQ4621174FDOQ4621174

Authors: Viorica Sofronie-Stokkermans 

Publication date: 8 February 2019

Published in: Scientific Annals of Computer Science (Search for Journal in Brave)

Abstract: In this paper we show that subsumption problems in lightweight description logics (such as $mathcalEL$ and $mathcal{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 $mathcalEL$, $mathcal{EL}^{+}$ and extensions thereof. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend $mathcalEL$ and $mathcal{EL}^{+}$ with $n$-ary roles and/or numerical domains. As a by-product, this allows us to show that the algebraic models of $calEL$ and ${calEL}^{+}$ have ground interpolation and thus that $calEL$, ${calEL}^{+}$, and their extensions studied in this paper have interpolation. We also show how these ideas can be used for the description logic $mathcal{EL}^{++}$.

Full work available at URL: https://arxiv.org/abs/1311.2973

Recommendations

• Locality and subsumption testing in \({\mathcal{EL}}\) and some of its extensions
• Representation theorems and locality for subsumption testing and interpolation in the description logics \(\mathcal{EL}\), \(\mathcal{EL}^+\) and their extensions with \(n\)-ary roles and numerical domains
• Local completeness logic on Kleene algebra with tests
• Local applications of logics via model-theoretic interpretations
• Notions of locality and their logical characterizations over finite models
• scientific article; zbMATH DE number 1961525
• Algebraization, parametrized local deduction theorem and interpolation for substructural logics over FL
• Local entailment test in the reachability problem for well-structured transition systems
• Logics for extensional, locally complete analysis via domain refinements
• scientific article; zbMATH DE number 5592264

zbMATH Keywords

deductiondescription logicshierarchical reasoning

Mathematics Subject Classification ID

Knowledge representation (68T30) Logic in artificial intelligence (68T27) Semilattices (06A12)

Cited In (5)

• Local collection and end-extensions of models of compositional truth
• Representation theorems and locality for subsumption testing and interpolation in the description logics \(\mathcal{EL}\), \(\mathcal{EL}^+\) and their extensions with \(n\)-ary roles and numerical domains
• A Proof-Theoretic Approach to Deciding Subsumption and Computing Least Common Subsumer in $\cal EL$ w.r.t. Hybrid TBoxes
• Locality and subsumption testing in \({\mathcal{EL}}\) and some of its extensions
• KI 2005: Advances in Artificial Intelligence

This page was built for publication: Locality and Applications to Subsumption Testing in EL and Some of its Extensions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4621174)