Education-oriented Proof Assistant Based on Calculational Logic: Proof Theory Algorithms and Assessment Experience
DOI:
https://doi.org/10.19153/cleiej.26.2.6Keywords:
Algorithm Proof Theory, Calculational Logic, Interactive Theorem Prover, Education, Propositional Logic, Boolean Algebras, Finite Difference, Combinatory Logic.Abstract
This work presents an interactive proof assistant, based on Dijkstra-Scholten logic, aimed at teaching logic and discrete mathematics in higher education. The assistant interface is web and easy to use, since inferences can be made just with the mouse. The educational experience is presented showing a correlation between the grades of the assessments in class and those made with the application web. Additionally, an algorithm proof theory for the Disjktra-Scholten system are made and the following algorithms are shown: 1) a versatile printing algorithm that allows the administrator to configure the symbols of a theory, by assigning the desired presentation with LaTeX; 2) An algorithm, based on Broda and Damas combinators, for generate monotonic or anti monotonic inferences in the Dijkstra-Scholten logic; 3) An algorithm to generate the proofs of dual theorems in Boolean Algebra theory.
References
E. W. Dijkstra and S. C. Scholten, Predicate calculus and program semantics. New York: Texts and
Monographs in Computer Science, Springer-Verlag, 1990.
D. Gries and F. B. Schneider, A logical approach to discrete math. New York, New York: Springer,
F. Flaviani, “Interactive theorem prover based on calculational logic to assist finite difference and
summation learning,” In: Uskov V.L., Howlett R.J., Jain L.C. (eds) Smart Education and e-Learning
Smart Innovation, Systems and Technologies, vol. 240, pp. 161–172, 2021.
S. Broda and L. Damas, “Compact bracket abstraction in combinatory logic,” The Journal of Symbolic
Logic, vol. 62, no. 1, pp. 729–740, 1997.
L. Bijlsma and R. Nederpelt, “Dijkstra-scholten predicate calculus: Concepts and misconceptions,”
Acta Informatica, vol. 35, pp. 1007–1036, 1998.
D. Gries and F. B. 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,” Journal 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. 13–28, 2009.
D. Gries and F. Schneider, “Formalizations of substitution of equals for equals,” Cornell University,
NY, Tech. Rep. TR98-1686, May 1998.
V. Lifschitz, “On calculational proofs,” Annals of Pure and Applied Logic, vol. 113, no. 1, pp. 207–224,
E. W. Dijkstra, “The everywhere operator once more,” Austin University, TX, Tech. Rep. EWD1086,
Nov. 1990.
R. Dijkstra, ““everywhere” in predicate algebra and modal logic,” Information Processing Letters,
vol. 58, no. 5, pp. 237–243, 1996.
D. Gries and F. B. Scheneider, “Adding the everywhere operator to propositional logic,” Journal of
Logic and Computation, vol. 8, no. 1, pp. 119–130, 1998.
D. Gries, “Foundations for calculational logic,” Mathematical Methods in Program Development, NATO
ASI Series F: Computer and System Sciences, vol. 8, pp. 83–126, 1997.
J. Girard, P. Taylor, and Y. Lafont, Proof and types. Cambridge, London: Cambridge university press,
H. Simmons, Derivation and Computation: taking the Curry-Howard correspondence seriously. Cambridge,
London: Cambridge university press, 2000.
M. S0/rensen and P. Urzyczyn, Lectures on the Curry-Howard isomorphism. Amsterdam, The Netherlands:
Elsevier, 2006.
K. Broda. (2009) slides of automated reasoning course. imperial college, london. [Online]. Available:
https://www.doc.ic.ac.uk/?kb/MACTHINGS/SLIDES/0LIntro4up.pdf
T. Nipkow, L. Paulson, and M. Wenzel. (2015) Isabelle/hol: A proof assistant for higher-order-logic.
[Online]. Available: http://isabelle.in.tum.de/dist/Isabelle2015/doc/tutorial.pdf
A. Mercer, A. Bundy, H. Duncan, and D. Aspinall, “Pg tips: A recommender system for an interactive
theorem prover,” in In Mathematical User-Interfaces Workshop (MathUI 2006), Oxford, London, Aug.
, pp. 290–294.
Y. Bertot and P. Cast´eran, Interactive Theorem Proving and Program Development:Coq Art: The
Calculus of Inductive Constructions. Berlin, Heidelberg: Springer-Verlag, 2004.
W. Kahl, “The teaching tool calccheck: A proof-checker for gries and schneider’s “logical approach to
discrete math”,” Certified Programs and Proofs, LNCS, Springer, vol. 7086, pp. 216–230, 2011.
——, “Calccheck: A proof checker for teaching the “logical approach to discrete math”,” in: Avigad
J., Mahboubi A. (eds) Interactive Theorem Proving. Proc. 9th ITP Oxford. Lecture Notes in Computer
Science, vol. 10895, pp. 324–341, 2018.
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.
K. A. A. Gamage, E. K. D. Silva, and N. Gunawardhana, “Online delivery and assessment during
covid-19: safeguarding academic integrity,” Educ. Sci., vol. 10, no. 11, pp. 301–324, 2020.
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.
J. Villadsen, F. Halkjaer, and A. Schlichtkrull, “Natural deduction assistant (nadea),” in In Pedro
Quaresma & Walther Neuper, editors: Proceedings 7th International Work-shop on Theorem proving
components for Educational Software (ThEdu), EPTCS 290, Oxford, UK, Jul. 2019, pp. 14–29.
[Online]. Available: https://doi.org/10.4204/EPTCS.290.2
S. Sch¨onfinkel, “¨uber die bausteine der mathematischen logik,” Mathematische Annalen, vol. 92, pp.
–316, 1924.
H. Curry, F. R., and C. W., Combinatory Logic, volume 1. North-Holland, 1958.
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.
F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge: Cambridge University Press,
J. 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.
K. Rosen, Discrete Mathematics and Its Applications (7 ed.). New York: McGraw-Hill Higher Education,
Mathjax documentation. [Online]. Available: https://docs.mathjax.org/en/latest
F. Flaviani and E. Tahhan, “Criteria for bracket abstractions design,” Electronic Notes in Theoretical
Computer Science, vol. 349, pp. 25–48, 2020.
M. Bunder, “Expedited broda-damas bracket abstraction,” Journal of Symbolic Logic, vol. 64, no. 4,
pp. 1850–1857, 2000.
A. Baldor, Algebra de Baldor. Publicaciones Cultural, 2002.
J. Hoffmann, Selecci´on de Temas de Matem´aticas. Sphinx, 1995.
F. Scheid and R. Di Costanzo, M´etodos Num´ericos. Mexico: McGraw-Hill, 1991.
Downloads
Published
Issue
Section
License
Copyright (c) 2023 Federico Flaviani, Walter Carballosa
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).
