SAT Encoding of Unification in $\mathcal{ELH}_{{R}^+}$ w.r.t. Cycle-Restricted Ontologies

DOI10.1007/978-3-642-31365-3_5zbMath1358.68280OpenAlexW2142835256MaRDI QIDQ2908475

Stefan Borgwardt, Franz Baader, Barbara Morawska

Publication date: 5 September 2012

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-31365-3_5

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Knowledge representation (68T30) Mechanization of proofs and logical operations (03B35)

Related Items

Deciding unifiability and computing local unifiers in the description logic \(\mathcal{EL}\) without top constructor, Optimal fixed-premise repairs of \(\mathcal{E}\mathcal{L}\) TBoxes, Extending Unification in $\mathcal{EL}$ to Disunification: The Case of Dismatching and Local Disunification, Most specific consequences in the description logic \(\mathcal{E} \mathcal{L} \)