Fehler in direkten Beweisen (Transformationen)

Formale Fehler

1. Der Startbaum stimmt nicht mit dem linken Baum der Aufgabenstellung überein.
2. Der letzte Ergebnisbaum stimmt nicht mit dem rechten Baum der Aufgabenstellung überein.
3. Die Variable einer Substitution ist nicht im ADT definiert.
4. Die Sorte der Variable einer Substitution und des Baums mit dem sie substituiert werden soll, stimmen nicht überein.
5. Die Sorte des Ergebnisbaums stimmt nicht mit der Sorte des vorherigen Baums überein

Inhaltliche Fehler

6. Der angegebene Unterterm ist kein Unterterm des vorherigen Baums. D.h., der Unterterm ist Falsch.
7. Der Unterterm passt auf keine der Seiten des Axioms, es ist also der Unterterm oder das Axiom falsch.
8. Der Unterterm passt nur auf die Endseite des Axioms. D.h., die Richtungsangabe ist falsch.
9. Der Unterterm passt auf die Startseite des Axioms, aber die Substitution ist falsch.
10. Der Unterterm passt nur auf die Endseite des Axioms und die Substitution ist falsch. Die Richtungsangabe ist auch falsch.
11. Der Unterterm passt auf die Startseite des Axioms, die Substitution ist korrekt, wurde aber falsch angewandt, sodass der Ergebnisbaum falsch ist.
12. Der Unterterm passt nur auf die Endseite des Axioms, die Substitution ist dafur korrekt, der Unterterm wurde nicht korrekt durch die substituierte Startseite des Axioms ersetzt, sodass der Ergebnisbaum falsch ist. Die Richtungsangabe ist auch falsch.

Warnungen

13. Eine oder mehrere Variablen, die in der Substitution angegeben worden sind, welche mit einem Baum substituiert werden sollen, können nicht in dem angegebenen Axiom gefunden werden.

Fehler im Zusammenhang mit Lemmata

Formale Fehler

20. Ein Lemma hat zyklische Abhängigkeiten. Demnach ist das Lemma unbewiesen, außer das Lemma entspricht einer Aufgabenstellung.
21. Im Transformationsschritt wird ein unbewiesenes Lemma angewandt oder es wird ein Lemma aus der Aufgabenstellung entgegen der topologischen Ordnung angewandt. Demnach ist der Transformationsschritt falsch.
22. Ein Lemma, dessen Name mit einem zu beweisenden Lemma übereinstimmt, stimmt inhaltlich nicht mit dem zu beweisenden Lemma überein. Demnach ist die entsprechende Aufgabenstellung nicht erfüllt.

Inhaltliche Fehler

23. Ein Lemma, welches von der Aufgabenstellung vorgegeben wurde, ist fur den Hauptbeweis nicht nützlich eingesetzt.

Fehler im Zusammenhang mit struktureller Induktion

Formale Fehler

30. Es wird eine Induktion über eine feste Variable geführt.
31. Im Beweis wird eine Induktionsvariable gewählt, welche keine Konstruktoren hat.
32. Ein Induktionsfall fehlt.
33. Es liegt ein ungültiger / doppelter Induktionsfall vor.
34. Die Gleichung eines Induktionsfalls oder einer Induktionshypothese ist nicht korrekt.
35. Eine Variable, die fest sein soll wird allquantifiziert.
36. Induktionshypothese wird im Induktionsanfang angewandt.
37. Bei Anwendung einer Regel wird eine feste Variable substituiert.
38. Die Induktionsvariable stimmt nicht mit der Induktionsvariable der Aufgabenstellung überein.
39. Bei vorgegebener Induktionsvariable wird eine Transformation als Beweis verwendet.

Inhaltliche Fehler

40. Eine Variable, die allquantifiziert sein soll, wird als fest angegeben.
41. Die Angabe der Art des Induktionsfalls ist inkonsistent zur Wahl des Konstruktors.

Warnungen

42. Es liegt eine doppelte Induktionshypothese vor.
43. Die aufbauende Variable der Induktionshypothese wird in keinem Induktionsfall als solche eingesetzt.