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 *
* *
***************************************