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 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.