Discrete Mathematics: A Constructive Approach

Contents:

• 1. Introduction
  • 1.1. Mathematical Maturity
  • 1.2. Logical Reasoning
  • 1.3. Role in Computer Science
  • 1.4. Automated Reasoning
  • 1.5. Course Content and Organization
• 2. Logic
  • 2.1. Introduction
  • 2.2. Terms
  • 2.3. Types
  • 2.4. Functions
  • 2.5. Propositions
  • 2.6. Predicates
• 3. Proofs
  • 3.1. Introduction
  • 3.2. Equality
  • 3.3. Forall
  • 3.4. False
  • 3.5. True
  • 3.6. Conjunction
  • 3.7. Implication
  • 3.8. Bi-Implication
  • 3.9. Disjunction
  • 3.10. Negation
  • 3.11. Exists
• 4. Induction
  • 4.1. Example
  • 4.2. Data Types
  • 4.3. Functions & Recursion
  • 4.4. Induction
  • 4.5. Parameterized Types
  • 4.6. Polymorphic Pairs
  • 4.7. Boolean Algebra
  • 4.8. Natural Numbers
  • 4.9. Binary Trees
  • 4.10. Certified ADTs (Optional)
• 5. Informality
  • 5.1. Case Study
  • 5.2. Direct Proof
  • 5.3. Proof by Contradiction
  • 5.4. Proof by Induction
  • 5.5. Proof by Contraposition
  • 5.6. Summary
  • 5.7. Exercises
• 6. Sets
• 7. Automata
• 8. Languages
• 9. Satisfiability
• 10. Appendix 1: Set Up
  • 10.1. Installing Lean
  • 10.2. Cloning the Class Repository
  • 10.3. Using Your IDE
  • 10.4. Creating New Lean Projects
• 11. Appendix 2: Unix
  • 11.1. Unix: A Brief History
  • 11.2. Command-Line Commands
• 12. Acknowledgements

Indices and tables

• Index
• Module Index
• Search Page