Do exist programs to verify demostrations in logic?

Question

I am a universitary teacher of logic and I´m interested to design an create a program to verify demostrations about propositional and predicate logic to my students, but I want to know if programs to do that really exist and how works that. If you know about some program, or how works the code, you will helpme a lot. Thanks.

Answer 1

There are lots of proof assistants out there, e.g. Lean, Coq, Agda. If you're new to this stuff, I think you'll like Lean, because its syntax is fairly intuitive and there are online tutorials on the website.

Answer 2

From what I've read, theorem provers are "typed variants of the $\lambda$ calculus". On the other hand there are logic languages such as Prolog. Prolog is a programming language with "roots in first order logic". So depending on the focus of your course(s), one or the other might be better (program focused on theorem proving vs a language focused on first order logic).

As an example of Prolog, this statement demonstrates implication where the antecedent is true: "known(Q) :- known(P), known(implies(P, Q))"