Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
To: induc@cs.uiowa.edu, mind@aisb.ed.ac.uk, info-hol@cs.uidaho.edu
Subject: HOL/Nqthm Interface
Date: Thu, 23 Sep 93 10:40:05 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:191210:930923094016"@cl.cam.ac.uk>

The following may be of interest to the inductive theorem proving and HOL
communities:

During a recent visit by me to Computational Logic Inc., Matt Kaufmann, J Moore,
and I discussed what might be gained from linking HOL and Nqthm. It was clear
that Nqthm would be able to prove some useful first-order lemmas for HOL.
However, such theorems probably don't arise much in HOL proofs because the terms
present are usually higher-order. This prompted me to suggest some higher-order
HOL definitions and theorems that I thought it would be difficult for Nqthm to
deal with. However, Matt and J found a way to translate these into Nqthm that
looked as though it would be mechanizable. Matt then improved on the technique
so that Nqthm's recursion analysis was being fully exploited. This suggested
that there was some promise in the approach, so we discussed with Mike Gordon
the possibility of a collaboration to pursue the ideas.

The outcome is that there is a strong possibility that J Moore will visit
Cambridge for a few weeks next summer to develop an initial prototype interface.
If that produces good results then a longer-term project might be sought to
develop a properly engineered interface and to investigate the semantic issues
involved in `mixing' theorems from the two different logics.

Richard Boulton
University of Cambridge Computer Laboratory