Xref: utzoo sci.logic:832 comp.lang.prolog:2786
Path: utzoo!attcan!uunet!samsung!dali.cs.montana.edu!uakari.primate.wisc.edu!zaphod.mps.ohio-state.edu!rpi!uupsi!sunic!nuug!ulrik!humanist.uio.no!jtl
From: jtl@humanist.uio.no
Newsgroups: sci.logic,comp.lang.prolog
Subject: Automated higher order logic
Message-ID: <1990Jun7.164927.2631@ulrik.uio.no>
Date: 7 Jun 90 16:49:27 GMT
Sender: news@ulrik.uio.no (USENET News System)
Organization: University of Oslo
Lines: 14


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.