Introduction to Formal Reasoning (COMP2009)

• 1. Introduction
  • 1.1. Interactive proof systems
  • 1.2. Lean
• 2. Propositional logic
  • 2.1. What is a proposition?
  • 2.2. Our first proof
  • 2.3. Using assumptions
  • 2.4. Proof terms
  • 2.5. Conjunction
  • 2.6. The Currying Equivalence
  • 2.7. Disjunction
  • 2.8. Logic and algebra
  • 2.9. True, false and negation
  • 2.10. Summary of tactics
• 3. Classical logic
  • 3.1. The de Morgan laws
  • 3.2. The law of the excluded middle
  • 3.3. Indirect proof
  • 3.4. Intuitionistic vs classical logic
• 4. Predicate logic
  • 4.1. Predicates, relations and quantifiers
  • 4.2. The universal quantifier
  • 4.3. The existential quantifier
  • 4.4. Another Currying equivalence
  • 4.5. Equality
  • 4.6. Classical Predicate Logic
  • 4.7. Summary of tactics
• 5. The Booleans
  • 5.1. Functions on bool
  • 5.2. Proving some basic properties
  • 5.3. Proving equations about bool
  • 5.4. Relating bool and Prop
• 6. The Natural Numbers
  • 6.1. Basic properties of ℕ
  • 6.2. Structural recursion
  • 6.3. Induction
  • 6.4. Addition and its properties
  • 6.5. Multiplication and its properties
  • 6.6. Some Algebra
  • 6.7. Ordering the numbers
  • 6.8. Decidability
• 7. Lists
  • 7.1. Basic properties of list
  • 7.2. The free monoid
  • 7.3. Reverse
  • 7.4. Insertion sort
• 8. Trees
  • 8.1. Expression trees
  • 8.2. Tree sort