Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 22 Apr 1993 12:40:27 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA23715;
          Thu, 22 Apr 93 04:24:40 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from tuminfo2.informatik.tu-muenchen.de 
          by ted.cs.uidaho.edu (16.6/1.34) id AA23710;
          Thu, 22 Apr 93 04:24:19 -0700
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <57663>;
          Thu, 22 Apr 1993 13:24:02 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8086>;
          Thu, 22 Apr 1993 13:23:50 +0200
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: schneide@ira.uka.de, info-hol@ted.cs.uidaho.edu
In-Reply-To: schneide's message of Thu, 22 Apr 1993 09:22:37 +0200 <9304220621.AA23277@ted.cs.uidaho.edu>
Subject: Powerful Rewriting
Message-Id: <93Apr22.132350met_dst.8086@sunbroy14.informatik.tu-muenchen.de>
Date: Thu, 22 Apr 1993 13:23:48 +0200


> Has anyone implemented rules, conversions or tactics for a more powerful
> rewriting? For example, associative and commutative rewriting would in
> some cases be helpful. Moreover, HOL's rewriting does only first-order
> matching, in some cases higher-order matching would be more useful.
> Last but not least I would like to know who has experience with E-unification
> in HOL?

I have implemented associative-commutative unification, matching and
rewriting in hol90. This is restricted to working on terms that are
"essentially single sorted first order terms", although polymorphism is
allowed.

Cheers,
Konrad.