- Titel
- A nice Cycle Rule for Goal-Directed E-unification
- Zitierfähige Url:
- https://nbn-resolving.org/urn:nbn:de:bsz:14-qucosa2-793172
- Schriftenreihe
- LTCS-Report
- Bandnummer
- 04-01
- Erstveröffentlichung
- 2004
- DOI
- https://doi.org/10.25368/2022.138
- Abstract (EN)
- In this paper we improve a goal-directed E-unification procedure by introducing a new rule, Cycle, for the case of collapsing equations, i.e. equations of the type x ≈ v where x ∈ Var (v). In the case of these equations some obviously unnecessary infinite paths of inferences were possible, because it was not known if the inference system was still complete if the inferences were not allowed into positions of x in v. Cycle does not allow such inferences and we prove that the system is complete. Hence we prove that as in other approaches, inferences into variable positions in our goal-directed procedure are not needed.
- Freie Schlagwörter (DE)
- E-Vereinigung, Zyklus, Gleichung
- Freie Schlagwörter (EN)
- E-unification, cycle, 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-793172
- Veröffentlichungsdatum Qucosa
- 31.05.2022
- Dokumenttyp
- Bericht
- Sprache des Dokumentes
- Englisch
- Lizenz / Rechtehinweis
CC BY 4.0