In my master's thesis, I describe use of the intercalation calculus in an automated theorem prover for the purposes of hint generation in proof construction software. See also Wilfried Sieg's paper, Normal natural deduction proofs (in classical logic) (with John Byrnes); Studia Logica 60, 1998, 67-106. The programming related to my thesis was in Java, which suited our purposes well (creating a cross-platform graphical tool).

On the other hand, the intercalation calculus can be expressed more directly in a functional language (OCaml). Whether this is an advantage is, of course, context dependent. In any case, here is a propositional logic automated theorem prover.

• Sourceforge project.

My masters thesis, Strategic Proof Tutoring in Logic, is online.

• Text (HTML).
• Text (PDF).
• Slides (PDF).

In the mostly online course Logic and Proofs, students learn to construct natural deduction proofs in the Carnegie Proof Lab, a computer-based proof construction environment. When given challenging problems, students have difficulty figuring out how the premises connect with the conclusion. Through use of a modification of the intercalation calculus, a strategy is provided to students on choosing which inference rules to apply in various circumstances. The strategy is also implemented in AProS, an automated theorem prover. In this thesis I describe how the Carnegie Proof Lab has been extended to provide three different modes of dynamic strategic proof tutoring, using AProS to help generate hints. The Explanation Tutor explains how tactics apply to partial proofs, the Walkthrough Tutor guides students through strategically constructed proofs, and the Completion Tutor provides on-demand strategic hints. When properly used, they should provide students with support in learning how to construct proofs in a strategic fashion.