Interactive Theorem Assistant for Learning ``A Logical Approach to Discrete Math'': Proof Theory and Assessment Experience
DOI:
https://doi.org/10.19153/cleiej.29.3.5Keywords:
Calculational Logic, Predicate Logic, Proof Theory, Lambda Calculus, Interactive Theorem Prover, EducationAbstract
CalcLogic is a proof assistant adapted for students of Calculational Logic. CalcLogic uses the same syntax and theorems as in Gries and Schneider's book, ``A Logical Approach to Discrete Math''. All proofs can be done by students using only the mouse, without the need to learn any language. To mechanize the assistant, a new proof theory for Calculational Logic is developed in this paper. This theory allows the loading of first-order theories axiomatized with an axiom schemes. Also is presented a study, using statistical evidence, that shows a significant improvement in learning Calculational Logic when the formative activities are made by means of the assistant.
References
E. W. Dijkstra and S. Scholten, Predicate calculus and program semantics. Texts and Monographs in Computer Science, Springer-Verlag, New York, 1990.
D. Gries and F. Schneider, A logical approach to discrete math. Springer. Springer, New York, 1993.
C. Homepage, http://nefud.ldc.usb.ve/CalcLogic, last accessed 2025/01/25.
F. Flaviani, Interactive theorem prover based on calculational logic to assist finite difference and summation learning," In: Uskov, V. L., Howlett, R. J. (eds.) Smart Education and e-Learning 2021. Smart Innovation, Systems and Technologies, vol. 240, no. -, pp. 161{172, 2021.
Federico Flaviani and Walter Carballosa, Proof assistant based on calcultional logic to assist the learning of propositional logic and boolean algebras," in In: XLVIII Latin American Computer Conference (CLEI) 2022, October 2022, pp. 1{9. Armenia, Colombia.
F. Flaviani and W. Carballosa, Education-oriented proof assistant based on calculational logic: Proof theory algorithms and assessment Experience," CLEI Electronic Journal, vol. 26, no. 2, pp. 1{28, 2023.
F. Flaviani, S. Carrasquel and D. Coronado, Interactive theorem assistant for learning calculational logic in the style of a logical approach to discrete math"," in In: LI Latin American Computer Conference (CLEI) 2025, October 2025, pp. Valparaiso, Chile.
A. Church, A set of postulates for the foundation of logic," Annals of mathematics, vol. 33, no. 2, pp. 346{666, 1932.
C. H and F. R., Combinatory logic, vol 1. North-Holland Publishing Company, Amsterdam, 1958.
E. W. Dijkstra, The everywhere operator once more," Austin University, TX, Tech. Rep. EWD1086, nov 1990.
D. Gries and F. Scheneider, Formalizations of substitution of equals for equals," Cornel University, NY, Tech. Rep. TR98-1686, may 1998.
P. C. Y. Bertot, Interactive theorem proving and program development: Coq Art: The calculus of inductive constructions. Berlin, Heidelberg: Springer-Verlag, 2004.
M. W. T. Nipkow, L. Paulson, http://isabelle.in.tum.de/dist/Isabelle2015/doc/tutorial.pdf, 2015.
L. De Moura, S. Kong, J. Avigad, F. Van Doorn, and J. von Raumer, The lean theorem prover (system description)," in International Conference on Automated Deduction. Springer, 2015, pp. 378{388.
W. A. Howard et al., The formulae-as-types notion of construction," To HB Curry: essays on combinatory logic, lambda calculus and formalism, vol. 44, pp. 479{490, 1980.
P. Martin-L¨of, An intuitionistic theory of types: Predicative part," in Studies in Logic and the Foundations of Mathematics. Elsevier, 1975, vol. 80, pp. 73{118.
L. Bijlsma and R. Nederpelt, Dijkstra-Scholten predicate calculus: Concepts and misconceptions," Acta Informatica, vol. 35, no. 1, pp. 1007{1036, 1998.
D. Gries and F. Scheneider, Equational propositional logic," Information Processing Letters, vol. 53, no. 3, pp. 145{152, 1995.
G. Tourlakis, A basic formal equational predicate logic - Part I," Bulletin of the Section of Logic, vol. 29, no. 1, pp. 43{56, 2000.
||, A basic formal equational predicate logic - Part II," Bulletin of the Section of Logic, vol. 29, no. 3, pp. 75{87, 2000.
||, On the soundness and Completeness of Equational Predicate Logics," J. of Logic and Computation, vol. 11, no. 4, pp. 623{653, 2001.
||, A new foundation of a complete boolean equational logic," Bulletin of the Section of Logic, vol. 38, no. 1, pp. 12{28, 2009.
V. Lifschitz, On calculational proofs," Annals of Pure and Applied Logic, vol. 113, no. 1, pp. 207{224, 2001.
R. Dijkstra, Everywhere" in predicate algebra and modal logic," Information Processing Letters, vol. 58, no. 5, pp. 237{243, 1996.
D. Gries, Foundations for calculational logic," Mathematical Methods in Program Development, NATO ASI Series F: Computer and System Sciences. Springer, Berlin, vol. 158, no. 1, pp. 83{126, 1997.
D. Gries and F. Scheneider, Adding the everywhere operator to propositional logic," J. Logic and Comp, vol. 8, no. 1, pp. 119{130, 1998.
K. Broda, (2009) slides of automated reasoning course. Imperial college, london. [Online]. Available:, https://www.doc.ic.ac.uk/ kb/MACTHINGS/SLIDES/0LIntro4up.pdf.
A. Mercer, A. Bundy, H. Duncan, D. Aspinall, Pg tips: A recommender system for an interactive theorem prover," in In: Mathematical User-Interfaces Workshop (MathUI 2006), Aug. 2006, pp. 290{294. Oxford, London.
W. Kahl, The teaching tool calccheck a proof-checker for gries and schneider’s logical approach to discrete math"," in International Conference on Certified Programs and Proofs. Springer, 2011, pp.216{230.
||, Calccheck: a proof checker for teaching the logical approach to discrete math"," in International Conference on Interactive Theorem Proving. Springer, 2018, pp. 324{341.
A. Mendes and J. F. Ferreira, Towards verified handwritten calculational proofs," in: Avigad J., Mahboubi A. (eds) Interactive Theorem Proving. Proc. 9th ITP Oxford. Lecture Notes in Computer Science, vol. 10895, pp. 432{440, 2018.
S. B¨ohne and C. Kreitz, Learning how to prove: From the coq proof assistant to textbook style," in P. Quaresma and W. Neuper (Eds.): 6th International Workshop on Theorem proving components for Educational software (ThEdu 17) EPTCS 267, Gothenburg, Sweden, Aug. 2017, pp. 1{18.
H. Simmons, Derivation and Computation: taking the Curry-Howard correspondence seriously. Cambridge University Press, 2000.
H. Curry, The universal quantifier in combinatory logic," Annals of mathematics, vol. 32, no. 1, pp. 154{180, 1931.
G. Frege, Begriffsschrift, 1879. Translated in: From Frege to Godel, J. van Heijenoort (ed.). Harvard University Press, 1967.
J. A. Boh´orquez, Intuitionistic Logic according to Dijkstra’s Calculus of Equational Deduction," Notre Dame Journal of Formal Logic, vol. 49, no. 4, pp. 361{384, 2008.
S. Broda and L. Damas, Compact Bracket Abstraction in Combinatory Logic," The Journal of Symbolic Logic, vol. 62, no. 1, pp. 729{740, 1997.
F. Flaviani and J. E. Tahhan, Criteria for Bracket Abstraction Design," Electronic Notes in Theoretical Computer Science, vol. 349, no. 1, pp. 25{48, 2020.
M. Bunder, Expedited broda-damas bracket abstraction," The Journal of Symbolic Logic, vol. 64, no. 4, pp. 1850{1857, 2000.[40] T. Johnsson, Lambda lifting: transforming programs to recursive equations. In Conference on Functional Programming Languages and Computer Architecture, Nancy. Jouannaud (editor). LNCS 201. Springer Verlag, 1985.
B. Russell and A. N. Whitehead, Principia Mathematica, Volume 1. Cambridge at the University Press, 1925.
D. Gries, A calculational proof of andrew’s challenge," Cornell University. Ithaca, New York, Ithaca, New York, Tech. Rep. 96-102, - 1996.
T. Tao, Machine-assisted proof," Notices of the American Mathematical Society, vol. 72, no. 1, pp. 6{13, January 2025.
Downloads
Published
Issue
Section
License
Copyright (c) 2026 Federico Flaviani, Jorge Baralt-Torrijos, Soraya Carrasquel, David Coronado
This work is licensed under a Creative Commons Attribution 4.0 International License.
CLEIej is supported by its home institution, CLEI, and by the contribution of the Latin American and international researchers community, and it does not apply any author charges whatsoever for submitting and publishing. Since its creation in 1998, all contents are made publicly accesibly. The current license being applied is a (CC)-BY license (effective October 2015; between 2011 and 2015 a (CC)-BY-NC license was used).
