Theorem Provers believed lost
The following theorem provers are not featured in the Theorem Prover Museum since they are believed lost - in the sense that we have looked for them and could not find the sources.
We list the systems and detail what we have done to find them. Should you have other leads, please contact Michael Kohlhase or just open an issue on our tracker. We would love to move the systems back from this list.
We list theorem proving systems and their known associates (for contact)
There are 3 provers in the listing below.
Automath
| note: | contacted Rob Nederpelt, Freek Wiedijk, and Fairouz Kamareddine, they would know. |
|---|
Paul Abraham's proof checker
| note: | In April 2017 Paul stated that he no longer has the stack of cards with the LISP code. |
|---|
The early Argonne provers AURA, LMA/ITP
| note: | Russ Overbeek says it is too much work to retrieve them from tapes that he knows to exist in the basement. |
|---|