Please note: Due to relocation, the server of the Mathematical Library Search Engine will be down until March 12.
ILF is a shell that facilitates the work with a variety of theorem provers. Currently, it has interfaces with the automated provers Discount, Protein, Setheo and Spass.
The development of ILF is supported by the Deutsche Forschungsgemeinschaft within the "Schwerpunktprogramm Deduktion". The last workshop of the Schwerpunkt was organized December 11/12 1997 by the ILF group in Berlin.
Within ILF several provers can work simultaneously on related problems in a local network. ILF will control the load of the network and distribute proof jobs in an appropriate way.
Interactive provers for tableaux logic and model elimination are available. These provers can be controled by proof tactics written in Prolog. The interactive theorem prover ProofPad in ILF automatically calls external theorem provers to solve subproblems.
ILF provides interactive and automated theorem provers with a unified graphical user interface. It can visualize the structure of hierarchies of concepts, proofs or formulas with the TreeViewer. The TreeViewer is a separate tool developed by the ILF group for visualizing labelled directed acyclic graphs. It can be downloaded here.
ILF can generate LaTeX manuscripts to display theories and proofs with ordinary mathematical notation. This facility is available for external users through the ILF mail server.
The manual for ILF (from 1994) is available.
The ILF Mathematical Library intends to collect definitions, theorems and proofs from various sources. As a first step it contains a number of articles from the Mizar Mathematical Library.
The ILF Mathematical Library Search Engine allows to download a notebook for the Mathematica computer algebra system, version 3.0. This notebook can connect Mathematica with the Mathematical Library of the ILF system. Then you can search some articles from the Mizar Mathematical Library for theorems on elementary set theoretic concepts. Automated theorem provers will assist your search.
Proof problems extracted from the Mizar Library and converted to TPTP first order format are available for downloading.
A set of typed proof problems extracted from the Mizar Library is announced in the AAR Newsletter, No. 42 January 1999.
Copyright © 1996 The ILF Group
Most recent revision 23. January 1999