- Titel
- Completeness of E-unification with eager Variable Elimination
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-790535
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 03-03
- Erstveröffentlichung
- 2003
- DOI
- https://doi.org/10.25368/2022.128
- Abstract (EN)
- The paper contains a proof of completeness of a goal-directed inference system for general E-unification with eager Variable Elimination. The proof is based on an analysis of a concept of ground, equational proof. The theory of equational proofs is developed in the first part. Solving variables in a goal is then shown to be reflected in defined transformations of an equational proof. The termination of these transformations proves termination of inferences with eager Variable Elimination.
- Freie Schlagwörter (DE)
- Gleichungslogik, Variableneliminierung, Beschreibungslogik, E-Vereinigung
- Freie Schlagwörter (EN)
- equational proof, variable elimination, description logic, E-unification
- 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-790535
- Veröffentlichungsdatum Qucosa
- 30.05.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0