# A nice Cycle Rule for Goal-Directed E-Unification

From International Center for Computational Logic

# A nice Cycle Rule for Goal-Directed E-Unification

##### B. MorawskaB. Morawska

B. Morawska

Technical Report,

**A nice Cycle Rule for Goal-Directed E-Unification**Technical Report,

*Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology*, volume LTCS-04-01, 2004.*LTCS-Report***Kurzfassung****Abstract**

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 appears in 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 is 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.**Bemerkung:****Note:**See http://lat.inf.tu-dresden.de/research/reports.html.**Forschungsgruppe:****Research Group:**Automatentheorie

```
@techreport{ Morawska-LTCS-04-01,
address = {Germany},
author = {B. {Morawska}},
institution = {Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology},
note = {See http://lat.inf.tu-dresden.de/research/reports.html.},
number = {LTCS-04-01},
title = {A nice Cycle Rule for Goal-Directed $E$-Unification},
type = {LTCS-Report},
year = {2004},
}
```