Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from dworshak.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 27 Sep 1993 10:30:26 +0100
Received: by dworshak.cs.uidaho.edu (1.37.109.4/16.2) id AA02877;
          Mon, 27 Sep 93 02:22:43 -0700
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA02873; Mon, 27 Sep 93 02:22:41 -0700
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <24368-0@iraun1.ira.uka.de>; Mon, 27 Sep 1993 10:22:24 +0100
Date: Mon, 27 Sep 93 10:24:53 MET
From: schneide <schneide@ira.uka.de>
To: info-hol@cs.uidaho.edu
Subject: HOL/Nqthm Interface
Message-Id: <"iraun1.ira.370:27.08.93.09.22.25"@ira.uka.de>

Hi,
  some people do consider the work in first-order theorem
proving in a higher order framework as not very worthful.
But as Richard pointed out, there are some ways how 
(sometimes) "higher-order" proof goals can be translated
into first-order goals which can then be (hopefully) proven
automatically.
  Anyone who is interested in this topic should consider the
article of Manfred Kerber on the IJCAI91 whose reference
I give below.


@techreport{Kerb90,
   author = {{M. Kerber}},
   institution = {University of Kaiserslautern},
   key = {Kerb90},
   number = {SR-90-19},
   title = {How to prove Higher Order Theorems in First Order Logic},
   type = {SEKI Report},
   year = {1990}
}

@inproceedings{Kerb91,
   author = {{M. Kerber}},
   booktitle = {Proceedings of the International Joint Conference on 
		Artificial Intelligence},
   key = {Kerb91},
   title = {How to Prove Higher Order Theorems in First Order Logic},
   year = {1991}
}