Hausaufgaben

empfohlen: beide (b), 4, 5

1. TeReSe Ex. 1.3.2

   Def: (→₁,→₂) kommutieren schwach: ←₁⋅→₂⊆→₂^*⋅←₁^*

   Def: (→₁,→₂) kommutieren: ←₁^*⋅→₂^*⊆→₂^*⋅←₁^*

   1. Satz: wenn (→₁,→₂) schwach kommutieren und SN(→₁∪→₂), dann kommutieren (→₁,→₂).
   2. Gegenbeispiel für: ...und SN(→₁)∧SN(→₂), dann ...

2. TeReSe Ex. 1.3.15, Geser 1990, di Cosmo, Piperno 1995
   1. Wenn ←₁⋅→₂⊆→₂⁺⋅←₁^* und SN(→₂), dann kommutieren (→₁,→₂).
   2. zeigen, daß SN(→₂) notwendig ist.

3. TeReSe Ex. 1.3.3, Rosen 1973.

   Def (sub-commutative) CR^≤1(→) : = ←⋅→⊆→^{0, 1}⋅←^{0, 1}

   Satz: aus →₁^*=→₂^* und CR^≤1(→₁) folgt CR(→₂).

4. TeReSe Ex 1.3.22.ii

   ein R mit WCR(R)∧UNR(R)∧¬UNC(R)

5. alle Gegenbeispiele zu vorigen Aussagen könnte man
   • durch passende autotool-Aufgaben übeprüfen oder
   • durch passenden Carpa-Aufruf bestimmen https://www.win.tue.nl/~hzantema/carpa.html
   —aber nur, falls es Gegenbeispiele mit endlichem Universum gibt. Das ist nicht immer der Fall.

   Geben Sie eine Eigenschaft vom Typ Prop an https://autotool.imn.htwk-leipzig.de/docs/autotool-collection-1.3/Rewriting-Abstract-Data.html#t:Prop, die

   • erfüllbar ist,
   • aber nicht endlich erfüllbar (d.h., mit endlichen Universum erfüllbar)
6. Implementierung in Carpa (2018?) mit https://gitlab.imn.htwk-leipzig.de/autotool/all0/-/blob/master/collection/src/Rewriting/Abstract/Solve.hs (2015?) vergleichen.

   Gemeinsamkeit: aussagenlogische Codierung. Unterschied: SAT/BDD. Auswirkungen?