Hausaufgaben

1. Beispiele für geometrische Theoreme aus Skript Gräbe 2018 (Simsonsche Gerade, Miquelscher Punkt, ...)
   • mit Geogebra zeichnen, Theorem überprüfen (durch Betrachtung der Lage bei Verschieben von Punkten)
   • algebraisieren (automatisieren!)
   • nach beschriebenen Verfahren lösen (Gröberbasis mit verschiedenen CAS ausrechnen)
2. ein falsches Theorem beweisen (um zu sehen, wie die Methode die Falsch-Aussage erkennt)
3. noch offene Aufgaben aus vorigen Wochen, insbesondere zur Eigenimplementierung von Polynomen (Division!) und Buchberger-Algorithmus
4. bad examples (für Buchberger-Algorithmus) in verschiedenen CAS (viele naive Algebraisierungen von geometrischen Sätzen ergeben aufwendige Rechnungen, aber es gibt auch kleinere schwere Testfälle)

   Beispiel (Verallgemeinerung? Quelle?)

   cyclic4 =
     let [a,b,c,d] = map (var . V) [1 .. 4]
     in  [ a*b*c*d-1
         , a*b*c+b*c*d+c*d*a+d*a*b
         , a*b+b*c+c*d+d*a
         , a+b+c+d
         ]
   

5. den Rabinovitch-Trick anwenden für den Satz über die Simson-Gerade in allgemeiner Lage (nur ein Punkt ist fixiert)

   fsimson = prove $ do
     ...
     return $ colinear a' b' c'
   

   die letzte Zeile ersetzen durch

     z0 <- number
     assert $ ...
     return $ ...
   

   und Laufzeiten (der naiven Implementierung sowie anderer CAS) vergleichen
6. die Behandlung von Degenerations-Bedingungen,

   Beispiel: der Satz von Pappus

   pappus = prove $ do
     a  <- point ; b  <- point; c  <- point_on a  b
     a' <- point ; b' <- point; c' <- point_on a' b'
     p <- intersection b c' b' c
     q <- intersection a c' a' c
     r <- intersection a b' a' b
     return $ -- degenerate cases:
              parallel (b-c') (b'-c)
            * parallel (a-c') (a'-c)
            * parallel (a-b') (a'-b)
              -- actual conclusion:
            * colinear p q r
   

7. bessere Implementierungen des Buchberger-Verfahrens: nicht jedesmal alle S-Polynome bestimmen und bezüglich aller bisherigen reduzieren.

   Zum Code in poly/Grobner.hs:

   • die Invarianten beweisen
   • die Termination begründen
     • für jede einzelne Reduktion eines (S-)Polynoms
     • für das gesamte Buchberger-Verfahren