Received: from leopard.cs.byu.edu (leopard.cs.byu.edu [128.187.2.182]) by ra.abo.fi (8.6.10/8.6.10) with ESMTP id QAA00628; Tue, 10 Oct 1995 16:27:39 +0200
Received: by leopard.cs.byu.edu
	(1.37.109.15/16.2) id AA213450445; Tue, 10 Oct 1995 07:07:25 -0600
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with ESMTP
	(1.37.109.15/16.2) id AA213420444; Tue, 10 Oct 1995 07:07:24 -0600
Received: from swan.cl.cam.ac.uk (swan.cl.cam.ac.uk [128.232.0.56]) by dworshak.cs.uidaho.edu (8.6.12/1.1) with ESMTP id GAA12627 for <info-hol@cs.uidaho.edu>; Tue, 10 Oct 1995 06:07:02 -0700
Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl;
          Tue, 10 Oct 1995 14:05:40 +0100
X-Mailer: exmh version 1.6.1 5/23/95
To: info-hol@cs.uidaho.edu
Subject: Unification/solving existential goals
In-Reply-To: Your message of "Mon, 09 Oct 1995 16:54:52 PDT." <199510092354.QAA19306@roma-cafe.cs.ucdavis.edu>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Date: Tue, 10 Oct 1995 14:05:31 +0100
From: Donald Syme <Donald.Syme@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:118710:951010130544"@cl.cam.ac.uk>


I'm looking for a HOL88 or HOL90 routine which, given
a term such as
    (--`?a b c. P1[a,b,c] /\ ... /\ Pn[a,b,c]`--)

and a list of available assumptions, will perform some
kind of backtracking unification against the assumptions to
find instances of a,b and c which satisfy all the conjuncts.  e.g. given
   [ |- P1 e f,
     |- P2 f g,
     |- !g. P3 e g]

and (--`?a b c. P1 a b /\ P2 b c /\ P3 a b`--)
I would like the routine to select 
	a -> e
	b -> f
	c -> g

Has anyone written something like this in HOL? Is this within 
the scope of your AC unification library, Konrad, or is it
simpler or more complex?  Would Isabelle eat this for breakfast (I
assume so)?

Don Syme