I've worked on a similar project (https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html), where the interface

I've worked on a similar project (https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html https://profs.info.uaic.ro/~stefan.ciobaca/lnd.html), where the interface allows only for backwards proofs. The only action allowed is to click a proof rule to be applied next, and the proof is presented in Fitch-like notation. Currently limited to propositional logic (not first-order).