Date: Mon, 29 May 95 12:52:25 +0200
From: dahn@mathematik.hu-berlin.de (Bernd Ingo Dahn)
Message-Id: <9505291052.AA12849@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Natural Language Output for Your Theorem Prover?
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

To whom it may concern

The mail server of the ILF system is now online for the public. It takes
model elimination proofs and returns natural language proof presentations
as LaTeX source. Proofs from other calculi can be presented if they have
been equipped with a block structure.

Moreover, a visualisation of the logical dependencies between the formulas 
in the proof can be delivered.

You can receive more detailed information by sending a message with text

help

to the ILF Server

ilf-serv@mathematik.hu-berlin.de

Then, the ILF Server will also tell you, how to obtain a version of the
Server documentation which is appropriate to your purposes.

Please, recall that the ILF Server is an experimental system and report
errors, problems, questions and suggestions for further improvements to

ilf-serv-request@mathematik.hu-berlin.de

I should be grateful, if you forward this message to anybody possibly
interested in the subject.

With best regards

Bernd, Ingo Dahn


***************************************
* Bernd, Ingo Dahn		      *
*				      *
* Humboldt-University		      *
* Institute of Pure Mathematics       *
* Ziegelstr. 13a		      *
* D-10099 Berlin		      *
*				      *
* Phone: (+49)30-2843-1829	      *
* Fax  : (+49)30-2843-1846            *
* Mail : dahn@mathematik.hu-berlin.de *
*				      *
***************************************