jtl@humanist.uio.no (06/07/90)
I have become interested in automated theorem proving/theorem provers/proof procedures for second (and eventually higher) order logics and will appreciate recommendations for readings. Survey papers in particular. Since higher order logic is incomplete, one has of course to give up something. I would like to give up as little as possible, and I am in particular looking for procedures that are complete with respect to the generalized (Henkin) models, or which at least respect extensionality. I have looked on some papers on lambdaProlog and the paper "Automating Higher-order Logic" by Andrews and al (84). As far as I can see their systems are not extensional though.
arshad@lfcs.ed.ac.uk (Arshad Mahmood) (06/08/90)
In article <1990Jun7.164927.2631@ulrik.uio.no> jtl@humanist.uio.no writes: > >I have become interested in automated theorem proving/theorem >provers/proof procedures for second (and eventually higher) order logics >and will appreciate recommendations for readings. Survey papers in >particular. > ..... > >I have looked on some papers on lambdaProlog and the paper "Automating >Higher-order Logic" by Andrews and al (84). As far as I can see their >systems are not extensional though. Well, there is a veritable industry in automating higher-order logic because of it's uses in Hardware Verification. Check out Mike Gordon's reports from the Computing Lab. at Cambridge University, you mention lambda prolog have you seen Dale Miller's thesis from Carnegie-Mellon. Sorry that I can't be of more help, but this is stuff I just happend to have absorbed through osmosis from the people around here. A. Mahmood LFCS Edinburgh University Scotland
mikef@lfcs.ed.ac.uk (Mike Fourman) (06/08/90)
There are systems for computer-assisted proof in (various) higher- order logic(s) under development and in use here at LFCS eg. LEGO (Pollack) LAMBDA (Abstract Hardwarte Ltd.) ISABELLE (Paulson) Prof. Michael P. Fourman email mikef@lfcs.ed.ac.uk Dept. of Computer Science 'PHONE (+44) (0)31-667 1081 X2733 JCMB, King's Buildings FAX (+44) (0)31 662 4712 Mayfield Road, Edinburgh EH9 3JZ, Scotland, UK
mahajan@fornax.UUCP (Sanjeev Mahajan) (06/13/90)
In article <1990Jun7.164927.2631@ulrik.uio.no>, jtl@humanist.uio.no writes: > > > Since higher order logic is incomplete, one has of course to give up ^^^^^^^^^^ By this, I presume you mean that Goedel's completeness theorem and Compactness theorem do not hold. Sanjeev