Novel Didactic Proof Assistant for First-Order Logic Natural Deduction
2014
We present a proof assistant designed to help learning formal proof, particularly in the system of Natural Deduction for First-Order Logic. The assistant handles formulas and derivations containing meta-variables and allows to maintain a library of instanciable lemmas. It possesses a graphical interface presenting proofs as trees and handles multiple simultaneous derivations that can be dragged and dropped into one another.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
11
References
0
Citations
NaN
KQI