“Teaching college students how to write rigorous proofs is a critical objective in courses that introduce formal reasoning. Over the course of several years, we have developed a mechanically-checkable style of calculational reasoning … to teach over a thousand freshman-level undergraduate students how to reason about computation in our ‘Logic and Computation’ class at Northeastern University. … Our calculational proof checker is integrated into ACL2s and is available as an Eclipse IDE plugin, via a Web interface and as a stand-alone tool. It automatically checks proofs for correctness and provides useful feedback.”

Find the paper and full list of authors at ArXiv.