@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
NAME: M E R I L L 

KEYWORDS: 

An Equational Reasoning System in Standard ML.
==============================================

Brian Matthews, 
Dept of Computing Science, The University of Glasgow
& Rutherford Appleton Laboratory.

A preliminary version of  MERILL is now available via anonymous ftp
from the University of Glasgow. This system written in Standard ML,
is a general purpose order-sorted equational reasoning system
which:

* Allows the user to declare their own object language.

* Allows AC-rewriting and AC-unification of terms and equations.

* Has several completion algorithms.

* Is built on a hierarchy of types, known as Order-Sorting.  This allows
  greater expressive is defining partial functions and error handling and 
  also efficiency of rewriting.   

* Allows the user to try different termination methods.

The system currently has a menu driven teletype interface.  
Future plans with this system include: extending the order-sorted
paradigm to allow greater flexibility through a system of dynamic sorts;
adding a tactic language to allow the user to set up and run 
equational reasoning tasks;  the extension for more and more powerful 
termination methods; building a window based user-interface, using X-windows,
to allow a greater ease of use of the system.  

A user manual in LaTeX dvi format is included in the release.

This release is an early one, and I expect that there will be many errors!
Please be patient with the system and please report to me if there are any 
errors, or suggestions for improving the design.

Obtaining the system.
---------------------

The system is available via anonymous ftp from the University of Glasgow,
ftp address: ftp.dcs.glasgow.ac.uk (130.209.240.50)

Sample session:

$ ftp ftp.dcs.glasgow.ac.uk
Connected to vanuata.dcs.glasgow.ac.uk.
220 vanuata FTP server (Version 6.12 Tue Oct 6 13:34:12 BST 1992) ready.
Name (ftp.dcs.glasgow.ac.uk:bmm): anonymous
331 Guest login ok, send e-mail address as password.
Password:
230 Guest login ok, access restrictions apply.
ftp> cd pub/merill
250 CWD command successful.
ftp> binary
200 Type set to I.
ftp> get src.tar.Z
200 PORT command successful.
150 Opening BINARY mode data connection for src.tar.Z (288271 bytes).
226 Transfer complete.
local: src.tar.Z remote: src.tar.Z
288271 bytes received in 25 seconds (11 Kbytes/s)
ftp> close
221 Goodbye.
ftp> quit
$ 

Contact:

Brian Matthews

Dept of Computing Science			   Systems Engineering
University of Glasgow 			Rutherford Appleton Laboratory
Glasgow 						       Chilton
G12 8QQ								Didcot
Scotland, 						 OXON OX11 0QX
U.K.								  U.K.	

brian@dcs.glasgow.ac.uk				      bmm@inf.rl.ac.uk

	
[Info source, date ]
Brian Matthews, August 1995


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%