Applying the LEAN Theorem Prover to Teach Mathematical Logic to Information Systems Students: A Case Study

• Willian B. Vaneli IFES
• Jefferson O. Andrade IFES

DOI: https://doi.org/10.5753/eries.2024.244646

Abstract

This paper investigates the use of the LEAN theorem prover in teaching mathematical logic to Information Systems students. Although the quantitative evaluation of the impact of LEAN on student learning was postponed due to a strike, this study documents in detail the implementation of propositional logic problems using LEAN. The focus is on the application of LEAN to solve selected problems and on the analysis of how the tool can be used to explore logical concepts. This approach serves as a basis for future empirical evaluations of the effectiveness of this methodology in teaching mathematical logic.

Keywords: Mathematical Logic, LEAN Theorem Prover, Information Systems Education, Computational Tools, Educational Methodology

References

Avigad, J., De Moura, L., and Kong, S. (2015). Theorem proving in lean. Release, 3(0):1–4.

Avigad, J., Hölzl, J., and Serafin, L. (2017). A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389–423.

Avigad, J., Lewis, R. Y., and van Doorn, F. (2020). Logic and Proof. Lecture notes for the course Logic and Mathematical Inquiry.

Avigad, J. and Massot, P. (2024). Mathematics in lean. Technical Report Release 0.1, Lean Community.

Charles Fadel, Maya Bialik, e. B. T. (2015). Four-Dimensional Education: The Competencies Learners Need to Succeed. Solution Tree Press.

Cherniavsky, J. and Heeren, C. (2017). Self-Adaptive Systems for Machine Intelligence. IGI Global.

De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. (2015). The LEAN theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer.

Feofiloff, P. and Szwarcfiter, J. L. (2009). Algoritmos e Estruturas de Dados. LTC.

Gersting, J. L. (2019). Fundamentos Matemáticos Para a Ciência Da Computação: Matemática Discreta e Suas Aplicações. LTC, Rio de Janeiro, RJ, 7ª edição edition.

Huth, M. and Ryan, M. (2007). Lógica Em Ciência Da Computação: Modelagem e Argumentação Sobre Sistemas. LTC - Livros Tecnicos E Cientificos Editora Lda.

Plainer, M. (2021). Practical study of visual studio code. techreport, Technical University of Munich.