MINLOG is a
proof assistant developed at the University of Munich by the team of
Helmut Schwichtenberg.
MINLOG is based on
first order
In mathematics and other formal sciences, first-order or first order most often means either:
* "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of high ...
natural deduction calculus. It is intended to reason about
computable functionals, using
minimal rather than
classical or
intuitionistic logic. The primary 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.
External links
MINLOG homepage
Proof assistants