🚀 go-pugleaf

I am trying to write a rewriter in Prolog, as part of a program refinement
system.  It occurs to me that others have probably done this kind of thing, 
so ...  

Can anyone point me to any available implementations of rewriting systems in 
Prolog, or any published descriptions of same?

Just to explain further what I want from this rewriter:  I want to use the
rewriter to simplify the kinds of formulas that arise as verification
conditions (or proof obligations) in program development/verification.  Thus,
it needs to be able to handle logical connectives, arithmetic, and any other
data types (sets, bags, sequences etc) that I care to define via a set of
(conditional) rewrite rules.  Ideally it should use AC matching to avoid the
need for associativity and commutativity laws.  The rewriter should simplify
"obvious" formulas to true, and others to a form where obvious bits,
redundancy etc have been eliminated, leaving a set of lemmas that I can prove
separately.  As far as possible, I would like these residual lemmas to retain
the notation and structure of the original -- which means that I don't want to
use normalisation procedures that introduce different operators and totally
discard the original structure.

Now I realise this is asking for a lot, but I thought it worth enquiring to
see if anyone else has done or is doing this kind of thing.

I would also appreciate any suggestions regarding techniques for reducing
redundancy in rewriting, eg ways of ordering rules so that we don't need to
try every rewrite rule against every subformula at every stage in the
simplification process.

Cheers
	Lindsay


--------------
Lindsay Groves                     On leave from:	
School of Mathematical Sciences    Department of Computer Science
University of Bath                 Victoria University of Wellington
Bath, England                      Wellington, New Zealand
ljg@maths.bath.ac.uk               lindsay@comp.vuw.ac.nz