A Solver and Tutoring Tool for Logical Proofs in Natural Deduction
Vlist, C.L. van der
MetadataShow full item record
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.