MINLOG is a
proof assistant
In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor ...
developed at the University of Munich by the team of
Helmut Schwichtenberg
Helmut Schwichtenberg (born 5 April 1942 in Żagań) is a German mathematical logician.
Schwichtenberg studied mathematics from 1961 at the FU Berlin and from 1964 at the University of Münster, where he received his doctorate in 1968 from D ...
.
MINLOG is based on
first order 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. This contrasts with Hilbert-style systems, which instead use ax ...
calculus. It is intended to reason about
computable functionals
Computability is the ability to solve a problem in an effective manner. It is a key topic of the field of computability theory within mathematical logic and the theory of computation within computer science. The computability of a problem is clos ...
, using
minimal rather than
classical or
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
. 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
In programming language semantics, normalisation by evaluation (NBE) is a style of obtaining the normal form of terms in the λ-calculus by appealing to their denotational semantics. A term is first ''interpreted'' into a denotational model of th ...
as an efficient
term rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or red ...
device.
External links
MINLOG homepage
Proof assistants