Re: Automated higher order logic

Article View: sci.logic

Article #128

#128

From: Arshad Mahmood
Date: Thu, 07 Jun 1990 22:26

25 lines
1455 bytes

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

Technical Details

Message-ID: <4571@castle.ed.ac.uk>

Path: arc1-ca.pugleaf.net!utzoo!utgpu!news-server.csri.toronto.edu!mailrus!uunet!mcsun!ukc!edcastle!lfcs!arshad

References: <1990Jun7.164927.2631@ulrik.uio.no>

Show Full Headers

Complete Article Headers

Path: arc1-ca.pugleaf.net!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

Reply to Parent Message