- Titel
- Finite Herbrand Models for Restricted First-Order Clauses
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-796198
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 19-07
- Erstveröffentlichung
- 2019
- DOI
- https://doi.org/10.25368/2022.256
- Abstract (EN)
- We call a Herbrand model of a set of first-order clauses finite, if each of the predicates in the clauses is interpreted by a finite set of ground terms. We consider first-order clauses with the signature restricted to unary predicate and function symbols and one variable. Deciding the existence of a finite Herbrand model for a set of such clauses is known to be ExpTime-hard even when clauses are restricted to an anti-Horn form. Here we present an ExpTime algorithm to decide if a finite Herbrand model exists in the more general case of arbitrary clauses. Moreover, we describe a way to generate finite Herbrand models, if they exist. Since there can be infinitely many minimal finite Herbrand models, we propose a new notion of acyclic Herbrand models. If there is a finite Herbrand model for a set of restricted clauses, then there are finitely many (at most triple-exponentially many) acyclic Herbrand models. We show how to generate all of them.
- Freie Schlagwörter (DE)
- Herbrand-Struktur, Beschreibungslogik, ExpTime
- Freie Schlagwörter (EN)
- Herbrand model, description logic, ExpTime
- 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-796198
- Veröffentlichungsdatum Qucosa
- 20.06.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0