Automated higher order logic

Article View: sci.logic

Article #129

#129

From: jtl
Date: Thu, 07 Jun 1990 16:49

14 lines
1133 bytes

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.

Technical Details

Message-ID: <1990Jun7.164927.2631@ulrik.uio.no>

Path:

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

Show Full Headers

Complete Article Headers

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