- Titel
- Finding Finite Herbrand Models
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-795243
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 11-04
- Erstveröffentlichung
- 2011
- DOI
- https://doi.org/10.25368/2022.182
- Abstract (EN)
- 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₀. The new algorithm has only worst-case exponential runtime, in contrast to the previous one which was even best-case exponential.
- Freie Schlagwörter (DE)
- FL₀, ExpTime, Beschreibungslogik, Sprachgleichung
- Freie Schlagwörter (EN)
- FL₀, ExpTime, description logic, language equation
- Klassifikation (DDC)
- 004
- Klassifikation (RVK)
- ST 136
- Publizierende Institution
- Technische Universität Dresden, Dresden
- Version / Begutachtungsstatus
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-795243
- Veröffentlichungsdatum Qucosa
- 16.06.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0