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. This paper presents a study, using statistical evidence, to determine whether Calculational Logic learning is effective when the formative activities are made by means of the assistant. The results show a significant improvement in learning for those who study using the assistant.

CalcLogic is an interactive web-based proof assistant for Dijkstra-Scholten Calculational Logic, initially conceived for educational purposes. The assistant has been adapted so that students can learn symbolic logic with a friendly user interface, using the Gries and Scheneider’s textbook classic A Logical Approach to Discrete Math (LADM). The same LADM theorems and exercises are found in the assistant, using the same notation. However, the content of this paper does not seek to study educational aspects, but rather to present the functional ideas that led to the implementation of the assistant. The aim is to show how a functional foundation of Calculational Logic allows for the implementation of an assistant capable of reasoning in mathematical theories beyond LADM. It was implemented, in a transparent way for the user, as a functional equational logic, i.e. all the statements are equalities of anonymous functions. This approach avoids the variable capture problem between quantifiers through the automatic renaming of bound variables at beta reductions and allows writing axiom schemes.

Through a friendly user interface it is possible to bring students closer to the proof assistants, so that they can use this type of software as educational tools. In this work CalcLogic is presented, a proof assistant based on Calculational Logic, to assist the teaching of Propositional Logic and Boolean Algebras. Additionally, the results of the educational experience are shown. The collected data shows a group of students for whom the tool has been useful, it also shows a high correlation with the classroom assessments.

Dijkstra recursively defined the predicate transformer wp. Then Gries for each expression Exp of the language, defined domain(Exp), which is a predicate that indicates the states in which Exp is defined. This predicate Gries added it to the recursive formula that defines wp for assignment, and subsequently other authors added it to the rule that recursively defines wp for IF, so that in the bibliography there are several versions of the definition of wp, with and without occurrence of domain. The present work shows an inference of the definition of wp, demonstrating that the occurrence of domain is necessary for wp in assignement, IF and DO. This inference is done through the GCL denotational semantics over the set theory ZF, showing that the classical formulas of Dijkstra to define wp in GCL using domain, are valid if the language of set theory is used to write the assertions.