LATPub710: 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=We show that finding finite Herbrand models for a restricted class of | |Abstract=We show that finding finite Herbrand models for a restricted class of first-order clauses is ExpTime-complete. A Herbrand model is called finite if it interprets all predicates by finite subsets of the Herbrand universe. The restricted class of clauses consists of anti-Horn clauses with monadic predicates and terms constructed over unary function symbols and constants. | ||
first-order clauses is ExpTime-complete. A Herbrand model is called finite if it | The decision procedure can be used as a new goal-oriented algorithm to solve linear language equations and unification problems in the description logic FL_0. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential. | ||
interprets all predicates by finite subsets of the Herbrand universe. The | |||
restricted class of clauses consists of anti-Horn clauses with monadic | |||
predicates and terms constructed over unary function symbols and constants. | |||
The decision procedure can be used as a new goal-oriented algorithm to solve | |||
linear language equations and unification problems in the description logic | |||
FL_0. The new algorithm has only worst-case exponential runtime, in contrast to | |||
the previous one which was even best-case exponential. | |||
|ISBN= | |ISBN= | ||
|ISSN= | |ISSN= | ||
| Zeile 43: | Zeile 35: | ||
year = {2011}, | year = {2011}, | ||
} | } | ||
}} | }} | ||
Version vom 23. März 2015, 13:24 Uhr
Finding Finite Herbrand Models
Stefan BorgwardtStefan Borgwardt, Barbara MorawskaBarbara Morawska
Stefan Borgwardt, Barbara Morawska
Finding Finite Herbrand Models
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, volume 11-04, 2011. LTCS-Report
Finding Finite Herbrand Models
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Technische Universität Dresden, volume 11-04, 2011. LTCS-Report
- KurzfassungAbstract
We show that finding finite Herbrand models for a restricted class of first-order clauses is ExpTime-complete. A Herbrand model is called finite if it interprets all predicates by finite subsets of the Herbrand universe. The restricted class of clauses consists of anti-Horn clauses with monadic predicates and terms constructed over unary function symbols and constants. The decision procedure can be used as a new goal-oriented algorithm to solve linear language equations and unification problems in the description logic FL_0. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential. - Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
- Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory
@techreport{ BoMo-LTCS-11-04,
address = {Dresden, Germany},
author = {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 = {11-04},
title = {Finding Finite {H}erbrand Models},
type = {LTCS-Report},
year = {2011},
}
