PropLogic.IntroElim

• Falsum
  • Einführung
  • Eliminierung
• Negation
  • Einführung
  • Eliminierung
• Konjunktion
  • Einführung
  • Eliminierung
• Disjunktion
  • Einführung
  • Eliminierung
• Implikation
  • Einführung
  • Eliminierung
• Biimplikation
  • Einführung
  • Eliminierung

PropLogic.Laws

• Triviale Biimplikationen
• Kommutativität
  • Konjunktion
  • Disjunktion
• Assoziativität
  • Konjunktion
  • Disjunktion
• Gesetze von De Morgan
• Weitere Implementierungen von Implikationen
  • Konjunktion
  • Disjunktion
• Distributivität von Konjunktion und Disjunktion
• Typische klassische Gesetze
• Idempotenz
  • Konjunktion
  • Disjunktion
• Absorbtion
  • Konjunktion
  • Disjunktion
• Neutrale Elemente
  • Konjunktion
  • Disjunktion
• Kontraposition & Modus Tollens
• Transitivität der Implikation
• Currying
• Gesetz von Peirce

PropLogic.SomeExamples

FOL.Forall

• Elimination
• Einführung
• Kombinierte Beispiele

FOL.Exists

• Einführung
• Eliminierung
• Kombinierte Beispiele

FOL.Groups

Induction.Intro

• Induktive Strukturen
  • Induktive Strukturen "im Alltag"
  • Natürliche Zahlen
  • Syntax von Aussagenlogik
• Rekursion
  • Addition auf NAT
  • Check auf zero
  • Atome in einer formula
  • Semantik von Aussagenlogik
  • Einschränkung der möglichen Formeln
• (Strukturelle) Induktion
  • Assoziativität von add
  • Beispiel: Kommutativität von add
  • Disjunktive Korrektheit

Induction.Multiplication

• Definition
• Beispiele
• Beweise
  • Hilfslemmatas
  • Kommutativität
  • Distributivität
  • Assoziativität

Induction.Gauss

Induction.ConjunctiveFalseness

• Einschränkung der Grammatik
• Beweis der konjunktiven Falschheit