LATPub718: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| Zeile 15: | Zeile 15: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract=Unification in Description Logics has been proposed as an inference service that can, | |Abstract=Unification in Description Logics has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the Description Logic EL, which is used to define several large biomedical ontologies, unification is NP-complete. An NP unification algorithm for EL based on a translation into propositional satisfiability (SAT) has recently been presented. In this report, we extend this SAT encoding in two directions: on the one hand, we add general concept inclusion axioms, and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the translation to be complete, however, the ontology needs to satisfy a certain cycle restriction. The SAT translation depends on a new rewriting-based characterization of subsumption w.r.t. ELHR+-ontologies. | ||
for example, be used to detect redundancies in ontologies. For the Description Logic EL, | |||
which is used to define several large biomedical ontologies, unification is NP-complete. | |||
An NP unification algorithm for EL based on a translation into propositional | |||
satisfiability (SAT) has recently been presented. In this report, we extend this SAT | |||
encoding in two directions: on the one hand, we add general concept inclusion axioms, | |||
and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the | |||
translation to be complete, however, the ontology needs to satisfy a certain cycle | |||
restriction. The SAT translation depends on a new rewriting-based characterization of | |||
subsumption w.r.t. ELHR+-ontologies. | |||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 44: | Zeile 34: | ||
year = {2012}, | year = {2012}, | ||
} | } | ||
}} | }} | ||
Version vom 23. März 2015, 13:24 Uhr
SAT Encoding of Unification in ELH_R^+ w.r.t. Cycle-Restricted Ontologies
Franz BaaderFranz Baader, Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska
Franz Baader, Stefan Borgwardt, Barbara Morawska
SAT Encoding of Unification in ELH_R^+ w.r.t. Cycle-Restricted Ontologies
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, volume 12-02, 2012. LTCS-Report
SAT Encoding of Unification in ELH_R^+ w.r.t. Cycle-Restricted Ontologies
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, volume 12-02, 2012. LTCS-Report
- KurzfassungAbstract
Unification in Description Logics has been proposed as an inference service that can, for example, be used to detect redundancies in ontologies. For the Description Logic EL, which is used to define several large biomedical ontologies, unification is NP-complete. An NP unification algorithm for EL based on a translation into propositional satisfiability (SAT) has recently been presented. In this report, we extend this SAT encoding in two directions: on the one hand, we add general concept inclusion axioms, and on the other hand, we add role hierarchies (H) and transitive roles (R+). For the translation to be complete, however, the ontology needs to satisfy a certain cycle restriction. The SAT translation depends on a new rewriting-based characterization of subsumption w.r.t. ELHR+-ontologies. - Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
- Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@techreport{ BaBM-LTCS-12-02,
address = {Dresden, Germany},
author = {Franz {Baader} and Stefan {Borgwardt} and Barbara {Morawska}},
institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universit{\"a}t Dresden},
note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
number = {12-02},
title = {{SAT} Encoding of Unification in {$\mathcal{ELH}_{R^+}$} w.r.t. Cycle-Restricted Ontologies},
type = {LTCS-Report},
year = {2012},
}
