Awatmath.1801
net.applic
utcsrgv!utzoo!decvax!watmath!cbostrum
Fri Feb 19 22:53:25 1982
LCF and similars
Someone in this newsgroup a while ago mentioned LCF.
I am wondering if anyone out there has any experience with this
system that they could let me know about. We have a copy of
a Franz Lisp version from Goteburg that runs on the VAX,
but not much has been done with it here. I find it quite interesting
except that I am upset by a fairly glaring problem in its logic, viz:
the inability to add predictates. You can add other constants,
but they are all function symbols. This means that you cannot
use logical formulas with NOT, OR, IFF, amongst others, in them.
You can define these things after a fashion, but they remain terms,
and cant be readily manipulated. Does anybody know anything about this
problem?
In general, I am interested in systems that could be considered
"aids to the working mathematician", in the sense of convenient
and helpful interaction, proof checking, and the ability to program
sophisticated proof strategies. LCF wins as a first start in some
ways, but in other ways it is dismal.
It wins because of the language ML that allows that programming
of proof techniques; this is lacking in the other systems I know of.
However, it seems to require an awful lot of detail, and its logic
is not too flexible, especially in terms of subsuming detail. Also,
it proof management schemes are vastly inferior to Affirm's, it seems.
Other systems I know a little about include Affirm (Gerhart, et al)
Automath (de Bruijn), FOL (Weyrauch).
I would like to hear from anybody interested in or doing work
(developing or using) such systems.
If anyone thinks this is sort of out of place material for this newgroup
(which unfortunately seems to be dead), I would be glad to explain why I
believe that it most certainly is not.
-----------------------------------------------------------------
gopher://quux.org/ conversion by John Goerzen <
[email protected]>
of
http://communication.ucsd.edu/A-News/
This Usenet Oldnews Archive
article may be copied and distributed freely, provided:
1. There is no money collected for the text(s) of the articles.
2. The following notice remains appended to each copy:
The Usenet Oldnews Archive: Compilation Copyright (C) 1981, 1996
Bruce Jones, Henry Spencer, David Wiseman.
