KalkulierbaR
Published:
KalkulierbaR is a webtool for teaching different proof calculi for predicate and first-order logic. It presents each calculus as a serious game and enables the students to quickly get feedback on proof attempts.
The tool is used in the Automated Theorem Proving at TU Darmstadt and the concept behind KalkulierbaR is described in our paper. The implementation, developed in several student projects, is available at github.