Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 20 Jan 1994 10:47:54 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA14671;
          Thu, 20 Jan 1994 03:40:18 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA14667;
          Thu, 20 Jan 1994 03:40:15 -0700
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA18623;
          Thu, 20 Jan 1994 02:36:26 -0800
Received: from guillemot.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 20 Jan 1994 10:30:33 +0000
To: Phil Windley <windley@leopard.cs.byu.edu>
Cc: info-hol@cs.uidaho.edu
Subject: Re: X_EXISTS_TAC
In-Reply-To: Your message of "Wed, 19 Jan 94 20:41:43 MST." <"swan.cl.cam.:141200:940120044551"@cl.cam.ac.uk>
Date: Thu, 20 Jan 94 10:30:12 +0000
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:004000:940120103516"@cl.cam.ac.uk>

> Of course, a conversion that proves permuting the variables doesn't change
> the meaning would be as good.

See SWAP_EXISTS_CONV in the main system. This works for just two quantifiers
but could be used to provide more extensive permutation.

Richard.