A nice Cycle Rule for Goal-Directed E-Unification

B. MorawskaB. Morawska

Datei:Morawska-LTCS-04-01.ps.gz

Download

B. Morawska
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

Details
Bibtex

KurzfassungAbstract
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: AutomatentheorieAutomata Theory

@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},
}