MinITP is a proof assistant dedicated to OCaml experiments about tactics.
It can also be used for pedagogic purposes: its logic is very simple (the
intuitionistic propositional logic but it will evolve) so it can be a nice introduction to proof assistants.
The code has to be well documented, so do not hesitate to give your feedbacks !
To compile the program, you need to type:
cd src
make
You need a version of OCaml with menhir and ocamllex.
Once the installation has been made, you can use the
propositional intuitionistic logic proof assistant:
./proplog
Alexis Carré, Louise Dubois de Prisque