Skip to content

Experiments with my own (very small) proof assistant

Notifications You must be signed in to change notification settings

GaliMouette/MinITP

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

51 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

MinITP

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 !

Installation and use

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

Authors

Louise Dubois de Prisque

About

Experiments with my own (very small) proof assistant

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • OCaml 98.8%
  • Makefile 1.2%