Herunterbrechen von Termgraphen Lösung von Gleichungen? Hilfsmittel: Unifikation Zwei Strategien: Minimales Zusammenfalten: Neue Regel nicht auf denselben Knoten anwenden Maximales Zusammenfalten: Nach jeder Regelanwedung -> Vollständig zusammengefalteter Graph Beispiel Regeln: exp(0) -> s(0) exp(s(x))-> exp(x) + exp(x) Anfrage: exp(x) =^? s(0)+...+s(0) (genau 2ⁿ mal) Beispiel(2) Literatur Alle genannten Fakten und alle verwendeten Darstellungen basieren auf D. Plump, Term Rewriting, 1999