Department Mathematik



The MINLOG System

About the MINLOG System

MINLOG is an interactive proof system developed by Helmut Schwichtenberg and members of the logic group at the University of Munich.

MINLOG is based on first order natural deduction calculus. It is intended to reason about computable functionals, using minimal rather than classical or intuitionistic logic. The main motivation behind MINLOG is to exploit the proofs-as-programs paradigm for program development and program verification. Proofs are in fact treated as first class objects which can be normalized. If a formula is existential then its proof can be used for reading off an instance of it, or changed appropriately for program development by proof transformation. To this end MINLOG is equipped with tools to extract functional programs directly from proof terms. This also applies to non-constructive proofs, using a refined A-translation. The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device.

How to get MINLOG

The latest beta version of MINLOG is available as a tar.gz file, from Subversion (for members of the working group) and as Debian packages.

To get an impression of the latest changes see the last log messages or download the SVN snapshot: minlog-latest.tar.gz.

MINLOG is implemented in SCHEME and runs under every SCHEME version supporting the Revised5 Report on the Algorithmic Language Scheme. MINLOG's favorite dialect is Petite Chez Scheme from Cadence Research Systems, which is freely distributed at the address

For further help to install MINLOG on your system, take a look at the installation instructions.


If you have any problems with the MINLOG system or suggestions please feel free to send an email to

MINLOG should not be confused with MINLOG, a theorem prover for propositional logic, by John Slaney at Australian National University. Also note that the URL is not!