Teaching Experience: Logic and Formal Methods with Coq

  • Martin Henz
  • Aquinas Hobor
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7086)


During the past three years we have been integrating mechanized theorem proving into a traditional introductory course on formal methods. We explain our goals for adding mechanized provers to the course, and illustrate how we have integrated the provers into our syllabus to meet those goals. We also document some of the teaching materials we have developed for the course to date, and what our experiences have been like.


Modal Logic Formal Method Propositional Logic Predicate Logic Intuitionistic Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Andrews, P.B., Bishop, P., Brown, C.E., Issar, S., Pfenning, F., Xi, H.: ETPS: A system to help students write formal proofs (2003)Google Scholar
  2. 2.
  3. 3.
    Asperti, A., Coen, C.S., Tassi, E., Zacchiroli, S.: User interaction with the matita proof assistant. Journal of Automated Reasoning 39(2), 109–139 (2007)CrossRefzbMATHGoogle Scholar
  4. 4.
    Aldrich, J., Simmons, R.J., Shin, K.: SASyLF: An educational proof assistant for language theory. In: 2008 ACM SIGPLAN Workshop on Functional and Declarative Programming Education (FDPE 2008), Victoria, BC, Canada (2008)Google Scholar
  5. 5.
    Ben-Ari, M.: Mathematical Logic for Computer Science. Springer, Heidelberg (2001)CrossRefzbMATHGoogle Scholar
  6. 6.
    Borchert, D.M. (ed.): Glossary of Logical Terms, 2nd edn. Encyclopedia of Philosophy. Macmillan (2006)Google Scholar
  7. 7.
    de Wind, P.: Modal logic in Coq. VU University Amsterdam, IR-488 (2001),
  8. 8.
    Henz, M., Hobor, A.: Course materials for cs3234/cs5209 (2010),
  9. 9.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)Google Scholar
  10. 10.
    Huth, M.R.A., Ryan, M.D.: Logic in Computer Science: Modelling and reasoning about systems. Cambridge University Press, Cambridge (2000)zbMATHGoogle Scholar
  11. 11.
    Nemhauser, G.L., Trick, M.A.: Scheduling a major college basketball conference. Operations Research 46(1), 1–8 (1998)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Ou, X., Govindavajhala, S., Appel, A.W.: MulVAL: A logic-based network security analyzer. In: 14th USENIX Security Symposium (2005)Google Scholar
  13. 13.
    Parry, W.T., Hacker, E.A.: Aristotelian Logic. State University of New York Press (1991)Google Scholar
  14. 14.
    Pierce, B.C.: Lambda, the ultimate TA: Using a proof assistant to teach programming language foundations (2009)Google Scholar
  15. 15.
    Zhang, H.: SATO: A decision procedure for propositional logic. Association of Automated Resasoning Newsletters 22 (1993, updated version of November 29) (1997)Google Scholar
  16. 16.
    Zhang, H.: Generating college conference basketball schedules by a SAT solver. In: Proceedings of the Fifth International Symposium on Theory and Applications of Satisfiability Testing, Cincinnati, Ohio, pp. 281–291 (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Martin Henz
    • 1
  • Aquinas Hobor
    • 1
  1. 1.National University of SingaporeSingapore

Personalised recommendations