MINLOG is a proof assistant developed at the University of Munich by the team of Helmut Schwichtenberg.

MINLOG is based on first order

First-order logic

First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first-order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic...

 natural deduction

Natural deduction

In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning...

 calculus. It is intended to reason about computable functionals, using minimal

Minimal logic

Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is a variant of intuitionistic logic that rejects not only the classical law of excluded middle , but also the principle of explosion .Just like intuitionistic logic, minimal logic can be...

 rather than classical

Classical logic

Classical logic identifies a class of formal logics that have been most intensively studied and most widely used. The class is sometimes called standard logic as well...

 or intuitionistic logic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

.
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.