MINLOG is a proof assistant and automated theorem prover based on minimal logic. It is developed primarily at the University of Munich. MINLOG focuses on extracting computational content from proofs, aiming to provide a practical approach to program synthesis from formal specifications.
Core Principles:
MINLOG is founded on the principle of proof interpretation, often referred to as the "formulas-as-types" or "Curry-Howard isomorphism." This isomorphism establishes a direct correspondence between logical proofs and executable programs. Specifically:
- Proofs as Programs: A proof of a formula corresponds to a program that satisfies the specification represented by that formula.
- Formulas as Types: A formula represents the type of the program derived from its proof.
Key Features:
- Minimal Logic: MINLOG's core logic is minimal logic, a constructive logic which, unlike classical logic, does not rely on the law of excluded middle (p or not p). This constructiveness is crucial for extracting computational content from proofs.
- Proof Extraction: MINLOG provides mechanisms to automatically extract programs from formal proofs. The extracted programs are guaranteed to satisfy the specification encoded in the proved formula.
- Interactive Proof Development: MINLOG supports interactive proof construction, allowing users to guide the theorem proving process.
- Automated Theorem Proving: MINLOG incorporates automated theorem proving techniques to assist in proof search and discovery.
- Term Rewriting: MINLOG features a term rewriting system used for simplifying and normalizing terms during proof construction and program extraction.
- Emphasis on Computability: MINLOG prioritizes computable solutions. The system focuses on extracting programs that are both correct and efficient.
Applications:
MINLOG is used in various areas including:
- Program Synthesis: Deriving correct-by-construction programs from formal specifications.
- Formal Verification: Verifying the correctness of existing programs by proving their adherence to formal specifications.
- Mathematics: Formalizing mathematical proofs and extracting computational content from them.
- Education: Teaching and exploring the relationship between logic and computation.
Current Status and Development:
MINLOG is actively developed and maintained. Its development is driven by research in proof theory, program synthesis, and formal verification. The system is continuously evolving with new features and improvements.