Integrating Logical Functions with ILF

Abstract

This is a description of the system ILF developed at the Humboldt-University at Berlin. ILF is a system that integrates automated theorem provers, proof tactics for interactive deductive systems and models within a graphical user interface. The structure and commands of ILF are presented. A special part is devoted to the TreeViewer _ a part of ILF used for visualising directed acyclic graphs, which can be used as a separate programme. We describe the possibilities to extend ILF by integrating more interactive and automated deductive systems. The last part describes the ProofPad - a sample configuration for editing proofs in the field of lattice ordered groups.