1994-03-01Buch DOI: 10.18452/2527
Integrating Logical Functions with ILF
Dahn, Bernd I.
Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, Institut für Mathematik
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.
Dateien zu dieser Publikation