search

theoremprover-museum / theoremprover-museum.github.io

https://theoremprover-museum.github.io
GNU General Public License v3.0
52 stars 7 forks source link

Added three provers for induction #20

Closed moajohansson closed 5 years ago

moajohansson commented 5 years ago

Addition of systems for automated induction: Hipster, HipSpec and IsaPlanner. Hipster is under development still, HipSpec and IsaPlanner are not actively developed, but should be possible to run following instructions in respective repositories.

kohlhase commented 5 years ago

Thank you very much. You say that

Hipster is under development still, HipSpec and IsaPlanner are not actively developed, but should be possible to run following instructions in respective repositories.

Then the latter two should be labeled as active=false. And you should also add status=museum so they at least appear on the museum page.

kohlhase commented 5 years ago

I have done the suggested changes myself, please look it the museum is as you expect. This puts HipSpec and IsaPlanner into the museum and Hipster into the active theorem provers.