A proof is represented as a set of Prolog readable facts. Details can be found in the section "The ILF Standard Proof Format" in any version of the manual of the ILF Mail Server. This manual can be obtained from the server by sending a mail with text 'help block' to ilf-serv@mathematik.hu-berlin.de. Users working with model elimination proofs should use the text 'help me' instead.
The ILF Server translates native output of the provers Otter, Setheo, KoMeT, Discount and ProCom/Capri into this unified format and might return the translated proofs on request.
The ILF system has also an experimental procedure (developed in cooperation with Czeslaw Bylinski from the MIZAR group) to translate articles from the MIZAR mathematical library into the ILF Standard Format.
Ingo Dahn