Hausaufgaben

empfohlen: jeder wenigstens eine konkrete Rechen-Aufgabe und eine Literatur-Aufgabe.

1. zu Folie Kritische Paare für TRS: kritische Paare ausrechnen.

   Passende wfmA angeben und vervollständigen (soweit möglich).

2. zu Folie Orthogonale Systeme: für das Beispiel nachrechnen: WCR, ¬CR.

   Das durch diese Regelmenge erzeugte ARS mit früheren Beispielen für WCR und ¬CR vergleichen.

3. Zeigen Sie Konfluenz von {1∨1→1, x∨y→y∨x}. Welche der in der VL genannten Sätze und Methoden sind hier anwendbar?
4. Beispiele und Beweis: die Dyck-Sprache ist die $\approx_{D}^{}$-Äquivalenzklasse von ε für D = {ab→ε}.

   Weil D konvergent ist (Beweis?) ist jede $\approx_{D}^{}$-Äquivalenzklasse durch eine D-Normalform charakterisiert.

   Diese D-Normaformen sind b^pa^q. Die D-Normalisierung ist also eine Abbildung f : {a, b}^*→$\mathbb {N}$².

   Für f (w₁) = (p₁, q₁) und f (w₂) = (p₂, q₂), geben Sie f (w₁⋅w₂) = (p, q) als Funktion von p₁, q₁, p₂, q₂ an.

   (Auf Deutsch: f ist ein Monoid-Homomorphismus von ({a, b}^*, ε,⋅) nach ($\mathbb {N}$²,(0, 0,),?) und das Fragezeichen ist gesucht. Recherche-Aufgabe: wie heißt dieses Ziel-Monoid?)

5. weitere Regeln für Inferenzsystem für Vervollständigung

   Siehe Winkler et al. (JAR 2013) https://www.uibk.ac.at/informatik/computational-logic/research/publications/publications-2013/pdfs/13jar2.pdf, Fig. 1, zitiert aus: Bachmair (TCS 1991).

   entsprechende Erweiterung der Autotool-Aufgabe diskutieren (...und realisieren als Masterarbeit)

   Vergleichen mit der Formulierung des Knuth-Bendix-Algorithmus in Huet (1980) https://hal.inria.fr/inria-00076536/file/RR-0025.pdf

6. Gruppendarstellungen und Anwendung von Knuth-Bendix: siehe Havas et al.: Some Challenging Group Presentations (J. Austr. Math. Soc., 1999) https://staff.itee.uq.edu.au/havas/1999hhkr.pdf

7. mit Original-Artikel von Knuth u. Bendix:
   • wie werden Terme notiert?
   • wo steht die Definition von KBO?
   • Vervollständigungsschritte nachrechnen (das Entstehen des CP sowie seine passende Orientierung)

   zur Geschichte von Knuth/Bendix siehe auch Donald Knuth: All Questions Answered, Notices Vol 49(3), https://www.ams.org/notices/200203/fea-knuth.pdf

8. (als Wiederholung und Ergänzung zu Termination) in KBO: welche Symbole dürfen Gewicht 0 haben? Warum die anderen nicht? (Gegen-Beispiele für SN( > ) angeben)

   TTT2 (Weboberfläche) kann auch KBO.