SpringerLink
Log in

Using Isabelle in Two Courses on Logic and Automated Reasoning

  • Conference paper
  • First Online:
Formal Methods Teaching (FMTea 2021)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 13122))

Included in the following conference series:

  • 538 Accesses

Abstract

We present our experiences teaching two courses on formal methods and detail the contents of the courses and their positioning in the curriculum. The first course is a bachelor course on logical systems and logic programming, with a focus on classical first-order logic and automatic theorem proving. The second course is a master course on automated reasoning, with a focus on classical higher-order logic and interactive theorem proving. The proof assistant Isabelle is used in both courses, using Isabelle/Pure as well as Isabelle/HOL. We describe our online tools to be used with Isabelle/HOL, in particular the Sequent Calculus Verifier (SeCaV) and the Natural Deduction Assistant (NaDeA). We also describe our innovative Students’ Proof Assistant which is formally verified in Isabelle/HOL and integrated in Isabelle/jEdit using Isabelle/ML.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 46.00
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 58.84
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Baanen, A., Bentkamp, A., Blanchette, J., Limperg, J., Hölzl, J.: The Hitchhiker’s Guide to Logical Verification (2020). https://github.com/blanchette/logical_verification_2020

  2. Bella, G.: You already used formal methods but did not know it. In: Dongol, B., Petre, L., Smith, G. (eds.) FMTea 2019. LNCS, vol. 11758, pp. 228–243. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-32441-4_15

    Chapter  Google Scholar 

  3. Ben-Ari, M.: Mathematical Logic for Computer Science. Springer, London (2012)

    Book  Google Scholar 

  4. Ben-Ari, M.: A Short Introduction to Set Theory (2020). https://www.weizmann.ac.il/sci-tea/benari/sites/sci-tea.benari/files/uploads/books/set.pdf

  5. Blanchette, J.C.: Formalizing the metatheory of logical calculi and automatic provers in Isabelle/HOL (invited talk). In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, 14–15 January 2019, pp. 1–13. ACM (2019)

    Google Scholar 

  6. Farmer, W.M.: The seven virtues of simple type theory. J. Appl. Log. 6(3), 267–286 (2008). https://doi.org/10.1016/j.jal.2007.11.001

    Article  MathSciNet  MATH  Google Scholar 

  7. From, A.H.: Formalizing Henkin-style completeness of an axiomatic system for propositional logic. In: Proceedings of the Web Summer School in Logic, Language and Information (WeSSLLI) and the European Summer School in Logic, Language and Information (ESSLLI) Virtual Student Session, pp. 1–12 (2020). Preliminary paper, accepted for Springer post-proceedings

    Google Scholar 

  8. From, A.H.: Epistemic logic: completeness of modal logics. Archive of Formal Proofs, October 2018. https://devel.isa-afp.org/entries/Epistemic_Logic.html, Formal proof development

  9. From, A.H.: Formalizing a Seligman-style tableau system for hybrid logic. Archive of Formal Proofs, December 2019. https://isa-afp.org/entries/Hybrid_Logic.html, Formal proof development

  10. From, A.H., Eschen, A.M., Villadsen, J.: Formalizing axiomatic systems for propositional logic in Isabelle/HOL. In: Kamareddine, F., Sacerdoti Coen, C. (eds.) CICM 2021. LNCS (LNAI), vol. 12833, pp. 32–46. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-81097-9_3

    Chapter  Google Scholar 

  11. From, A.H., Jacobsen, F.K., Villadsen, J.: SeCaV: a sequent calculus verifier in Isabelle/HOL. In: 16th International Workshop on Logical and Semantic Frameworks with Applications (LSFA 2021) – Presentation Only/Online Papers, pp. 1–16 (2021). https://mat.unb.br/lsfa2021/pages/lsfa2021_proceedings/LSFA_2021_paper_5.pdf

  12. From, A.H., Jensen, A.B., Schlichtkrull, A., Villadsen, J.: Teaching a formalized logical calculus. Electron. Proc. Theor. Comput. Sci. 313, 73–92 (2020). https://doi.org/10.4204/EPTCS.313.5

    Article  Google Scholar 

  13. From, A.H., Lund, S.T., Villadsen, J.: A case study in computer-assisted meta-reasoning. In: González, S.R., Machado, J.M., González-Briones, A., Wikarek, J., Loukanova, R., Katranas, G., Casado-Vara, R. (eds.) DCAI 2021. LNNS, vol. 332, pp. 53–63. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-86887-1_5

    Chapter  Google Scholar 

  14. From, A.H., Villadsen, J.: Teaching automated reasoning and formally verified functional programming in Agda and Isabelle/HOL. In: 10th International Workshop on Trends in Functional Programming in Education (TFPIE 2021) – Presentation Only/Online Papers, pp. 1–20 (2021). https://wiki.tfpie.science.ru.nl/TFPIE2021

  15. From, A.H., Villadsen, J., Blackburn, P.: Isabelle/HOL as a meta-language for teaching logic. Electron. Proc. Theor. Comput. Sci. 328, 18–34 (2020). https://doi.org/10.4204/eptcs.328.2

    Article  Google Scholar 

  16. Grover, S.: Toward a framework for formative assessment of conceptual learning in K-12 computer science classrooms. In: Proceedings of the 52nd ACM Technical Symposium on Computer Science Education, SIGCSE 2021, pp. 31–37 (2021). https://doi.org/10.1145/3408877.3432460

  17. Hales, T.C.: Formal proof. Not. Am. Math. Soc. 55, 1370–1380 (2008)

    MathSciNet  MATH  Google Scholar 

  18. Hao, Q., et al.: Towards understanding the effective design of automated formative feedback for programming assignments. Comput. Sci. Educ. 1–23 (2021). https://doi.org/10.1080/08993408.2020.1860408

  19. Harrison, J.: Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 153–170. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055135

    Chapter  Google Scholar 

  20. Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge (2009)

    Book  Google Scholar 

  21. Jensen, A.B., Larsen, J.B., Schlichtkrull, A., Villadsen, J.: Programming and verifying a declarative first-order prover in Isabelle/HOL. AI Commun. 31(3), 281–299 (2018)

    Article  MathSciNet  Google Scholar 

  22. Krauss, A.: Defining Recursive Functions in Isabelle/HOL (2021). https://isabelle.in.tum.de/doc/functions.pdf

  23. Michaelis, J., Nipkow, T.: Formalized proof systems for propositional logic. In: Abel, A., Forsberg, F.N., Kaposi, A. (eds.) 23rd International Conference on Types for Proofs and Programs, TYPES 2017, Budapest, Hungary, 29 May–1 June 2017. LIPIcs, vol. 104, pp. 5:1–5:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  24. Nipkow, T.: Teaching semantics with a proof assistant: no more LSD trip proofs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 24–38. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27940-9_3

    Chapter  Google Scholar 

  25. Nipkow, T.: Programming and Proving in Isabelle/HOL (Tutorial) (2021). https://isabelle.in.tum.de/doc/prog-prove.pdf

  26. Nipkow, T.: Teaching algorithms and data structures with a proof assistant (invited talk). In: Hritcu, C., Popescu, A. (eds.) 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, Virtual Event, CPP 2021, Denmark, 17–19 January 2021, pp. 1–3. ACM (2021). https://doi.org/10.1145/3437992.3439910

  27. Nipkow, T., et al.: Functional Algorithms, Verified! (2021). https://functional-algorithms-verified.org/

  28. Nipkow, T., Eberl, M., Haslbeck, M.P.L.: Verified textbook algorithms. In: Hung, D.V., Sokolsky, O. (eds.) ATVA 2020. LNCS, vol. 12302, pp. 25–53. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-59152-6_2

    Chapter  MATH  Google Scholar 

  29. Nipkow, T., Klein, G.: Concrete Semantics - With Isabelle/HOL. Springer, Heidelberg (2014)

    MATH  Google Scholar 

  30. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  31. Paulson, L.C.: Computational logic: its origins and applications. Proc. R. Soc. A. 474(2210), 20170872 (2018). https://doi.org/10.1098/rspa.2017.0872

  32. Peltier, N.: A variant of the superposition calculus. Archive of Formal Proofs, September 2016. http://isa-afp.org/entries/SuperCalc.shtml, Formal proof development

  33. Pierce, B.C., et al.: Software Foundations – 6 Online Textbooks (2021). https://softwarefoundations.cis.upenn.edu/

  34. Reis, G.: Facilitating meta-theory reasoning (invited paper). In: Pimentel, E., Tassi, E. (eds.) Proceedings Sixteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Pittsburgh, USA, 16th July 2021. Electronic Proceedings in Theoretical Computer Science, vol. 337, pp. 1–12. Open Publishing Association (2021). https://doi.org/10.4204/EPTCS.337.1

  35. Schlichtkrull, A., Blanchette, J., Traytel, D., Waldmann, U.: Formalizing Bachmair and Ganzinger’s ordered resolution prover. J. Autom. Reason. 64(7), 1169–1195 (2020)

    Article  MathSciNet  Google Scholar 

  36. Schlichtkrull, A., Villadsen, J., From, A.H.: Students’ Proof Assistant (SPA). In: Quaresma, P., Neuper, W. (eds.) Proceedings 7th International Workshop on Theorem Proving Components for Educational Software, ThEdu@FLoC 2018, Oxford, United Kingdom, 18 July 2018. Electronic Proceedings in Theoretical Computer Science, vol. 290, pp. 1–13. Open Publishing Association (2018). https://doi.org/10.4204/EPTCS.290.1

  37. Villadsen, J.: A micro prover for teaching automated reasoning. In: Seventh Workshop on Practical Aspects of Automated Reasoning (PAAR 2020) – Presentation Only/Online Papers, pp. 1–12 (2020). https://www.eprover.org/EVENTS/PAAR-2020.html

  38. Villadsen, J.: Tautology checkers in Isabelle and Haskell. In: Calimeri, F., Perri, S., Zumpano, E. (eds.) Proceedings of the 35th Edition of the Italian Conference on Computational Logic (CILC 2020), Rende, Italy, 13–15 October 2020. CEUR Workshop Proceedings, vol. 2710, pp. 327–341. CEUR-WS.org (2020). http://ceur-ws.org/Vol-2710/paper-21.pdf

  39. Villadsen, J., From, A.H., Schlichtkrull, A.: Natural Deduction Assistant (NaDeA). In: Quaresma, P., Neuper, W. (eds.) Proceedings 7th International Workshop on Theorem Proving Components for Educational Software, THedu@FLoC 2018, Oxford, United Kingdom, 18 July 2018. EPTCS, vol. 290, pp. 14–29 (2018). https://doi.org/10.4204/EPTCS.290.2

  40. Villadsen, J., Schlichtkrull, A., From, A.H.: A verified simple prover for first-order logic. In: Konev, B., Urban, J., Rümmer, P. (eds.) Proceedings of the 6th Workshop on Practical Aspects of Automated Reasoning (PAAR 2018) co-located with Federated Logic Conference 2018 (FLoC 2018), Oxford, UK, 19 July 2018. CEUR Workshop Proceedings, vol. 2162, pp. 88–104. CEUR-WS.org (2018). http://ceur-ws.org/Vol-2162/paper-08.pdf

  41. Wenzel, M.: The Isabelle/Isar Reference Manual (2021). https://isabelle.in.tum.de/doc/isar-ref.pdf

  42. Wenzel, M.: Isar—a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167–183. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48256-3_12

    Chapter  Google Scholar 

Download references

Acknowledgements

We thank Asta Halkjær From for comments on drafts. We thank the three anonymous reviewers whose comments and suggestions helped improve the paper.

Author information

Authors and Affiliations

  1. Technical University of Denmark, Kongens Lyngby, Denmark

    Jørgen Villadsen & Frederik Krogsdal Jacobsen

Authors
  1. Jørgen Villadsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frederik Krogsdal Jacobsen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jørgen Villadsen .

Editor information

Editors and Affiliations

  1. INESC-ID & IST, University of Lisbon, Lisbon, Portugal

    João F. Ferreira

  2. INESC TEC and University of Beira Interior, Covilhã, Portugal

    Alexandra Mendes

  3. McMaster University, Hamilton, ON, Canada

    Claudio Menghi

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Villadsen, J., Jacobsen, F.K. (2021). Using Isabelle in Two Courses on Logic and Automated Reasoning. In: Ferreira, J.F., Mendes, A., Menghi, C. (eds) Formal Methods Teaching. FMTea 2021. Lecture Notes in Computer Science(), vol 13122. Springer, Cham. https://doi.org/10.1007/978-3-030-91550-6_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-91550-6_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-91549-0

  • Online ISBN: 978-3-030-91550-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation