What was the first proof assistant? What was it used for? When and by who was it created? Is it still used today? And what was its purpose?
$\begingroup$
$\endgroup$
1
-
2$\begingroup$ Since computers and programs technically appeared before electric devices, the answer might probably be a little bit blurry... $\endgroup$– Trebor ♦Commented Feb 8, 2022 at 18:52
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
2
Arguably, the first theorem prover was the Logic Theorist, developed by a team at RAND back in the 1950s, which was used to generate alternate proofs for parts of Russell and Whitehead's Principia.
If you want to see what it looked like, I had a friend at RAND ask the archivist scan the July 12, 1956 revised version of the P-868 technical report which is 68 pages long (an earlier draft is online, too).
Russell wrote a short note to team, which was saved in the RAND archives:
Fan Mail...
Plas Penrhyn
Penrhyndeudraeth
Merioneth2 November, 1956
Dear Mr. Simon,
Thank you for your letter of October 2 and for the very interesting enclosure (RAND P-868). I am delighted to know that Principia Mathematica can now be done by machinery. I wish Whitehead and I had known of this possibility before we both wasted ten years doing it by hand. I am quite willing to believe that everything in deductive logic can be done by a machine.
Yours Very Truly,
Bertrand Russell
Although it's not used anymore (it was written in assembly for the Johnniac), it inspired the Lisp programming language.
-
7$\begingroup$ Perhaps add the year, which seems to be 1956. $\endgroup$ Commented Feb 8, 2022 at 21:17
-
2$\begingroup$ I add the original technical report; if someone wants to try to make a new version... $\endgroup$ Commented Feb 9, 2022 at 18:26
$\begingroup$
$\endgroup$
6
The first (1968) fibrational proof assistant for computers is known to be AUTOMATH prover which was implemented under the lead of Nicolaas Govert de Bruijn (AUT-68). It's the direct ancestor of the "type theoretical" line of proof assistants from which the better known current ones are NuPRL and Coq. The last version is known to be AUT-QE and released under the lead of Freek Wiedijk.
Modern provers of that family nowadays usually use Calculus of Construction with full set of rules, while AUT-68 was using only $\star \leadsto \Box$, but was lacking $\Box \leadsto \Box$. So today we usually take PTS/CoC for educational purposes but not AUT-68.
If you want to feel the type system of proto-provers you should dive into Henk: A Typed Intermediate Language by Simon Peyton Jones and Erik Meijer. As for stable known implementations I would suggest Morte for Haskell by Gabriella Gonzalez and its faster port to Erlang — PTS$^\infty$ by Groupoid.
As for non-fibrational provers in the style of Principia Mathematica (1910), you also can find a lot of implementations, and we also have one for educational purposes — PRINCIPIA, a logical system whose (almost) only inference rule is the substitution rule. It is insipired by Metamath and some Metamath-like systems.
-
4
-
2$\begingroup$ In this context $\mathbf{dependently\ typed}$, a thing able to express $\star \leadsto \Box$ from Lambda Cube (the generalization of $\lambda$-calculi given by Henk Barendregt). So the first computer prover was dependently typed! $\endgroup$ Commented Feb 8, 2022 at 23:28
-
2$\begingroup$ “Modern provers nowadays use Calculus of Construction” oh, the burn felt by the HOL and Isabelle users. I guess the line before that clarifies things, but maybe write “Modern provers of that family” $\endgroup$ Commented Feb 9, 2022 at 12:54
-
$\begingroup$ You have an objection that HOL/Isabell is not a modern prover? From usual udestanding for me e.g. Andromeda is modern, HOL is not. I just said like you said: from ‘that family’ $\mathbf{fibrational\ provers}$. $\endgroup$ Commented Feb 9, 2022 at 12:56
-
$\begingroup$ I concur with @JoachimBreitner, though I'm not a direct HOL user (in any of its flavours). $\endgroup$ Commented Feb 9, 2022 at 18:27
$\begingroup$
$\endgroup$
0
I regard "proof assistant" as synonymous with "interactive theorem prover", which rules out many of the systems mentioned in other answers. For example, the input to AUTOMATH was a deck of punched cards. AUTOMATH was a milestone but it was not a proof assistant.
I believe that the Boyer/Moore theorem prover was interactive from the start, though it may have supported a batch mode as well. Commands consisted of axioms, requests to prove particular formulas, and hints concerning rewriting. Boyer and Moore published this work originally in 1975. And it continues to this day in the form of ACL2.
Another very early system was Weyhrauch's FOL. It was an interactive proof checker for first-order logic. I never saw the point even back in the 1970s, since FOL is both inexpressive and easily automated.
The first recognisably modern proof assistant is undoubtedly Edinburgh LCF, which introduced the architecture on which most of today's proof assistants are closely based, especially those of the HOL family. Mike Gordon traces the evolution here.
