Completness of E-unification with eager Variable Elimination

B. MorawskaB. Morawska

Datei:Morawska-LTCS-03-03.ps.gz

Download

B. Morawska
Completness of E-unification with eager Variable Elimination
Technical Report, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, volume LTCS-03-03, 2003. LTCS-Report

Details
Bibtex

KurzfassungAbstract
The report 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.
Bemerkung: Note: See http://lat.inf.tu-dresden.de/research/reports.html.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@techreport{ Morawska-LTCS-03-03,
  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-03-03},
  title = {Completness of $E$-unification with eager Variable Elimination},
  type = {LTCS-Report},
  year = {2003},
}