LATPub705: Unterschied zwischen den Versionen
Aus International Center for Computational Logic
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
Marcel Lippmann (Diskussion | Beiträge) KKeine Bearbeitungszusammenfassung |
||
| (2 dazwischenliegende Versionen desselben Benutzers werden nicht angezeigt) | |||
| Zeile 5: | Zeile 5: | ||
}} | }} | ||
{{Techreport | {{Techreport | ||
|Title=SAT Encoding of Unification in | |Title=SAT Encoding of Unification in EL | ||
|Year=2010 | |Year=2010 | ||
|Month= | |Month= | ||
| Zeile 15: | Zeile 15: | ||
}} | }} | ||
{{Publikation Details | {{Publikation Details | ||
|Abstract=The Description Logic EL is an inexpressive knowledge representation language, | |Abstract=The Description Logic EL is an inexpressive knowledge representation language, which nevertheless has recently drawn considerable attention in the knowledge representation and the ontology community since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, EL is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in EL is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power. | ||
which nevertheless has recently drawn considerable attention in the knowledge representation | In this paper, we introduce a new NP-algorithm for solving unification problem in EL, which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state of the art SAT solvers when implementing an EL-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that EL-unification is in NP that is much simpler than the one given in our previous paper on EL-unification. | ||
and the ontology community since, on the one hand, important inference problems such as | |||
the subsumption problem are polynomial. On the other hand, EL | |||
is used to define large biomedical ontologies. Unification in | |||
Description Logics has been proposed as a novel inference | |||
service that can, for example, be used to detect redundancies | |||
in ontologies. | |||
In a recent paper, we have shown that unification in EL | |||
is NP-complete, and thus of a complexity that is considerably lower | |||
than in other Description Logics of comparably restricted expressive power. | |||
In this paper, we introduce a new NP-algorithm for solving unification problem in EL, | |||
which is based on a reduction to satisfiability in propositional logic (SAT). | |||
The advantage of this new algorithm is, on the one hand, that it allows us to employ | |||
highly optimized state of the art SAT solvers when implementing an EL-unification algorithm. | |||
On the other hand, this reduction provides us with a proof of the fact that EL-unification | |||
is in NP that is much simpler than the one given in our previous paper on EL-unification. | |||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 52: | Zeile 35: | ||
year = {2010}, | year = {2010}, | ||
} | } | ||
}} | }} | ||
Aktuelle Version vom 25. März 2015, 16:34 Uhr
SAT Encoding of Unification in EL
Franz BaaderFranz Baader, Barbara MorawskaBarbara Morawska
Franz Baader, Barbara Morawska
SAT Encoding of Unification in EL
Technical Report, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, volume 10-04, 2010. LTCS-Report
SAT Encoding of Unification in EL
Technical Report, Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universität Dresden, volume 10-04, 2010. LTCS-Report
- KurzfassungAbstract
The Description Logic EL is an inexpressive knowledge representation language, which nevertheless has recently drawn considerable attention in the knowledge representation and the ontology community since, on the one hand, important inference problems such as the subsumption problem are polynomial. On the other hand, EL is used to define large biomedical ontologies. Unification in Description Logics has been proposed as a novel inference service that can, for example, be used to detect redundancies in ontologies. In a recent paper, we have shown that unification in EL is NP-complete, and thus of a complexity that is considerably lower than in other Description Logics of comparably restricted expressive power. In this paper, we introduce a new NP-algorithm for solving unification problem in EL, which is based on a reduction to satisfiability in propositional logic (SAT). The advantage of this new algorithm is, on the one hand, that it allows us to employ highly optimized state of the art SAT solvers when implementing an EL-unification algorithm. On the other hand, this reduction provides us with a proof of the fact that EL-unification is in NP that is much simpler than the one given in our previous paper on EL-unification. - Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
- Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@techreport{ BaMo-LTCS-10-04,
address = {Dresden, Germany},
author = {Franz {Baader} and Barbara {Morawska}},
institution = {Chair of Automata Theory, Institute of Theoretical Computer Science, Technische Universit{\"a}t Dresden},
note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
number = {10-04},
title = {SAT Encoding of Unification in $\mathcal{EL}$},
type = {LTCS-Report},
year = {2010},
}
