- title
- Completeness of E-unification with eager Variable Elimination
- Please use the following URL when quoting:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-790535
- Series
- LTCS-Report
- multivolume_volume0
- 03-03
- publication_date
- 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.
- Keywords (DE)
- Gleichungslogik, Variableneliminierung, Beschreibungslogik, E-Vereinigung
- Keywords (EN)
- equational proof, variable elimination, description logic, E-unification
- Classification (DDC)
- 004
- Classification (RVK)
- ST 136
- university_publisher
- Technische Universität Dresden, Dresden
- version
- angenommene Version / Postprint / Autorenversion
- URN Qucosa
- urn:nbn:de:bsz:14-qucosa2-790535
- Qucosa date of publication
- 30.05.2022
- Document type
- report
- Document language
- English
- licence
CC BY 4.0