Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9206021335.AA08222@ted.cs.uidaho.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Public domain version of the prover FAUST
Date: Tue, 2 Jun 92 13:07:25 GMT
From: kumar@de.uka.ira

Hi!
At long last we have been able to get a version of FAUST ready for public domain.
FAUST is a first-order automatic prover for proving statements within HOL. It is also
capable of handling limited higher-order statements as shown in the file, example.ml.

You can get a version of FAUST by anonymous ftp from our site:
	
	i80s12.ira.uka.de (129.13.18.22)

All files are available in the directory pub/FAUST, either separately or as a single file 
called faust.tar.Z which contains a compressed tar version of all the files. Note that when
ftp'ing the compressed tar version, the ftp mode is to be set as binary. The file READ-ME
gives a short description of the available files and their usage.

We are hopeful that this would be useful and we welcome further suggestions and comments.
We would also request you to send us an email when you have used it, so that we could
keep you in touch with the improvements in FAUST.

Additionally, if there is a wish we would also put it under the contrib directory at the
hol ftp site.

Hope you enjoy FAUST!

Best Wishes!
Klaus, Kumar and Thomas


*******************************************************************************
Ramayya Kumar				          | email: kumar@ira.uka.de 
Institut fuer Rechnerentwurf und Fehlertoleranz,  | Tel.: +49 (721) 608 4354
Fakultaet fuer Informatik, Universitaet Karlsruhe,| Fax: +49 (721) 370455
P.O. Box 6980, W-7500 Karlsruhe 1, 		  |
Germany					          |