Organization:

Alexa Crawls
Starting in 1996,

Alexa Internet has been donating their crawl data to the Internet Archive. Flowing in every day, these data are added to the

Wayback Machine after an embargo period.

Crawl data donated by Alexa Internet. This data is currently not publicly accessible

# The ILF System

## A Tool for the Integration of Logical Functions

*
***Please note:**
Due to relocation, the server of
the Mathematical Library Search Engine will be down
until March 12.

## The ILF System

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

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.

The **ILF** Group

ilfserv-request@mathematik.hu-berlin.de
Copyright © 1996 The **ILF** Group

Most recent revision 23. January 1999