Meta Topics

Software Technology: Logical Reasoning in Proof Assistants

Assumed Knowledge:
Learning Outcomes:
  • Use propositions in more complex ways
  • Build logical connectives to build propositions.
  • User tactics to construct proofs with more complex propositions.
  • Understand the source of some of Coq’s restrictions.

All the material for this topic is contained in the Logic in Coq chapter of Software Foundations.