The Technical Basis

of the Theorem Prover Museum is provided by GitHub the premier web-based GIT repository hosting service. The free-for-public hosting service of GitHub allows to provide separate repositories for the respective systems and give the respective authors and maintainers control over them, while promising long-term availability. The Museum web site is conveniently organized as a public repository via GitHub pages, with all data about systems centralized in a provers database file in YAML format.

We are grateful to GitHub.com for their service to the open source community.

How can you contribute?

• If you want to help with the site admin, the presentation of theorem provers, … We collect suggestions and plans on the the issue tracker of the web site repository.
• If you have access (and rights) to (the sources of) a system, you can “donate” them to the museum
  1. you give us a list of repository names, then I will make them for you unter http://github.com/theoremprover-museum
  2. you give us your GitHub account name, and we will make you admin to these repositories.
  3. you fill out the metadata of your provers in the form of our provers database
  4. done; that was all.
• If you know about the history of theorem proving just add metadata to our provers database; There are two ways to do this:
  1. directly edit provers.yml according to the README in the web interface and make a pull request (specify this at the very bottom of the edit page)
  2. or download provers.yml and send the updated version via e-mail.
• to request a system, do the same as above.
• if all else fails, please contact Michael Kohlhase.

Individual Contributors to the Theorem Prover Museum

The Theorem prover museum is a community effort, the current collection has been made possible by the following individuals:

• a discussion with Jaques Fleuriot and Alan Smaill at the University of Edinburgh in February 2016 and their immediate offer to help made Michael’s vague idea of a collection of theorem prover sources sufficiently concrete to get him started.
• Tom Wiesing (FAU Erlangen-Nürnberg) has helped with technical support for the setup and maintenance of the web site.
• William Farmer (McMaster University) supplied the first system: IMPS.
• Jörg Siekmann has been immediately supportive of the idea and organized the contribution of the MKRP (Markgraph Karl Refutation Procedure) and OMEGA systems.
• Wolfgang Bibel triggered colleagues and former members of his group to contribute and promised to look for source code of his early systems.
• Bob Veroff pointed Michael to the source of Otter, packaged Prover9, and helped make contact to the Argonne people for the early systems.