theoremprover-museum/theoremprover-museum.github.io

theoremprover-museum.github.io's Issues

metadata schema for theorem provers

We should develop a metadata schema for provers, implement it in provers.yml, collect the respective data, and show it on the web site (e.g. as a popup for the provers. I think we need the following fields for a start:

• maintainer [n] (last kwown maintainers)
• authors [n] (original authors)
• years (the years of active development)
• home system home page if it still exists
• languages programming languages used
• license if any

There is more information in the table at https://en.wikipedia.org/wiki/Automated_theorem_proving which could be relevant for our metadata schema.

Once we have the metadata, we can make derived listings from those, not just the chronological we have right now.

develop a standard repository layout so that we can have other things than just the source

we want to have

• papers and manuals (e.g. in subdir doc)
• images and videos, ... (e.g. in img
• an extended metadata file

and implement this on the existing repositories.

get endorsement from the AAR.

http://www.aarinc.org/

ALF

You could add this prover if it is not developed any more.
https://en.wikipedia.org/wiki/ALF_(proof_assistant)

MetaPRL is currently been maintained

The current repo is located at https://github.com/LdBeth/metaprl that I'm still doing improvements and bug fixes, revived from the repo from one of the original authors https://github.com/jyh/metaprl.

Autologic --> Most Wanted Prover Museum

Dear Prof Kohlhase,

How about adding Autologic from Neil Tennant?
https://theoremprover-museum.github.io/wanted/

I find:

Autologic
Shows how to program on a computer (in Prolog) the
effective skills taught in introductory and intermediate
logic courses. The topics include the relevance of relevance,
representing formulae and proofs, avoiding loops and blind
alleys, and other aspects. Of interest to computational
logicians, proof-theorists, cognitive scientists, and workers
in artificial intelligence. Distributed by Columbia U. Press.
Annotation copyright by Book News, Inc., Portland, OR
https://www.amazon.de/dp/0748603581

And here some usage:

There was at least person who even read the book:
% and I learnt a trick or two from Neil Tennant's "Autologic" book.
https://github.com/ptarau/TypesAndProofs/blob/master/third_party/dyckhoff_orig.pro

It could be that Autologic was heading towards
Logic of Paradox from Graham Priest, but I am
currently not yet sure whats the content of Autologic,
since I could not yet grab a copy, neither some
code snippets from it.

Best Regards

Mark Tarver's SEQUEL system 7.0 and 5.3

https://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/lang/lisp/code/tools/sequel/
turns out they were here all along

Information on Automath

Freek Wiedijk has the following information on Automath: http://www.cs.ru.nl/~freek/aut

It also includes a reimplementation by himself (presently version 4.2), which he might consider as "active".

build a group of activists and advisors

Jacques Fleuriot has already signed up.

make forks of external repositories in the TPM orga.

We have some cases, where we have external repositories for systems (e.g. PRESS for the historic systems). For the active systems there are mostly external repositories, sometimes even on departmental servers.

I would generally like to have a fork in the theoremprover-museum organization and keep that up to date automatically. Then we have a safety measure (KISS) when these repositories go away. There may even be a way to update from other (i.e. non-git) repository types (but this is a longer-term problem we can address when we need to).

dead link for lost provers

In the paper at https://arxiv.org/abs/1904.10414, there is a link [TPLb] whose URL 404s right now.

move to a Jekyll-based setup (easier to have news, ... )?

We should think about this. It seems to me that we only have to copy over the setup from ICMS or so.

Broken link on active systems

https://theoremprover-museum.github.io/wanted/active does not work: 404

Archive repos with software heritage

I have set up automated archival of all repos of an organisation by following https://archive.softwareheritage.org/api/1/origin/save/webhook/github/doc/. Maybe this can be done for the theoremprover-museum organisation as well?

open the museum

by announcing its existence, when we have a credible set of contents (at least 5, maybe 10). We should announce at the following venues

• CADE/IJCAR
• Maililng lists
• ???

build up the database of existing systems

We should build up the database provers.yml of existing provers (and possibly forks; see #12) , so that when they retire, we already have them for the museum.

Please, add PTS checker Yarrow

Please, add PTS checker Yarrow ( https://www.cs.ru.nl/~janz/yarrow/ ), their site once went down

mine the old theorem prover overview pages for systems

(if they still exist).

add proper css to the most wanted list

Thanks & DECLARE

Thank you for this site. I once had a dream of hunting down exotic archaic LCF theorem provers. So I'm impressed to see it already done.

If it would be welcome, at some point I'd like to donate the source code for DECLARE, a theorem prover described in my thesis here

https://www.repository.cam.ac.uk/handle/1810/252967

there are two repositories for SNARK

I guess the internal one should be removed.

Keep a list of active theorem provers?

Do we want to keep a list, then we know where to check when the become inactive.

Darwin and Gandalf source online

Hello,

Darwin and Gandalf are both listed on the "most wanted list". I noticed that the source code for both of them is available online.

Darwin is here: http://combination.cs.uiowa.edu/Darwin/#Download

Gandalf can be found among the CASC-18 entrants: http://tptp.cs.miami.edu/CASC/18/Entrants.html

Both claim to be GPL-licensed (for Darwin, at the webpage above; for Gandalf, in the README file as well as the files GPLGandalf/COPYING and Scm/COPYING), so it at least should be legal to distribute them. But I haven't spoken to the authors.

snark

1. instalable via quicklisp (http://quicklisp.org)
2. https://github.com/nilqed/SNARK