MINLOG is a proof assistant developed at the University of Munich by the team of Helmut Schwichtenberg.
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.
To this end, MINLOG is equipped with tools to extract functional programs directly from proof terms.
The system is supported by automatic proof search and normalization by evaluation as an efficient term rewriting device.