A Solver and Tutoring Tool for Logical Proofs in Natural Deduction
Summary
This paper introduces LEGEND, an interactive tutoring system which provides formal proofs in natural deduction and allows users to construct their own proofs. I describe the way LEGEND can be used, and I explain the algorithm it utilizes to construct proofs or create graphs of paths from premises to a conclusion.