Xref: utzoo sci.logic:831 comp.lang.prolog:2784
Path: utzoo!utgpu!news-server.csri.toronto.edu!mailrus!uunet!mcsun!ukc!edcastle!lfcs!arshad
From: arshad@lfcs.ed.ac.uk (Arshad Mahmood)
Newsgroups: sci.logic,comp.lang.prolog
Subject: Re: Automated higher order logic
Message-ID: <4571@castle.ed.ac.uk>
Date: 7 Jun 90 22:26:46 GMT
References: <1990Jun7.164927.2631@ulrik.uio.no>
Reply-To: arshad@lfcs.ed.ac.uk (Arshad Mahmood)
Organization: Laboratory for the Foundations of Computer Science, Edinburgh U
Lines: 25

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