To build DISCOUNT:

gunzip DISCOUNT2.0.tar.gz;tar -xf DISCOUNT2.0.tar;cd DISCOUNT2.0;make install

To build the tools for proof analysis and presentation:

gunzip PCLSTUFF.tar.gz; tar -xf PCLSTUFF.tar.gz;cd PCL;make depend;make

To build the tools for building and maintaining the knowledge base:

gunzip PCLSTUFF.tar.gz; tar -xf PCLSTUFF.tar.gz;cd LEARN;make depend;make

DISCOUNT will translate fine under Solaris 2.4/2.5. Edit
DISCOUNT2.0/Makefile.common to adapt it to Linux or SunOs (you'll even
find some comments in English language...). The LEARN- and PCL tools
will compile clean and without any modification under all tested
Operating Systems (Solaris 2.X, SunOs 4.1.X, Linux).

To use the complete system you need DISCOUNT2.0, PCL and LEARN in your
search path.

Unfortunatly, there is little current documentation for the current
version of DISCOUNT. Look at
http://wwwjessen.informatik.tu-muenchen.de/~schulz/bibliography.html
to find overview papers and some more in depth (but slightly out of
date) information. In particular, "Analysis and Representation of
Equational Proofs Generated by a Distributed Completion Based Proof
System" discusses most aspects of PCL and proof presentation, and
"Explanation Based Learning for Distributed Equational Deduction"
documents the first learning variant of DISCOUNT.

Have fun!

Stephan <schulz@informatik.tu-muenchen.de>