A Solver and Tutoring Tool for Logical Proofs in Natural Deduction
Publication date
Authors
DOI
Document Type
Bachelor Thesis
Metadata
Show full item recordCollections
License
CC-BY-NC-ND
Abstract
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.
Keywords
Tutoring Tool; ITS