Minlog
Minlog는 1990년대 초반 독일 뮌헨 대학교(LMU Munich)의 헬무트 슈비히텐베르크(Helmut Schwichtenberg) 교수와 그의 연구팀이 개발한 대화형 정리 증명기(Interactive Theorem Prover, 또는 Proof Assistant)다.
이 시스템의 핵심 목적은 수학적 증명으로부터 실행 가능한 프로그램을 직접 추출하는 ‘증명 추출(Program Extraction from Proofs)‘에 있다.
주요 특징
-
기초 논리 체계 (Minimal Logic) Minlog라는 이름은 최소 논리(Minimal Logic)에서 유래했다. 고전 논리(Classical Logic)나 직관주의 논리(Intuitionistic Logic)와 달리 부정의 공리적 성질을 최소화한 1차 최소 논리와 고차 유한 타입(Higher-order finite types) 계산법을 기반으로 작동한다.
-
프로그램 추출 (Program Extraction) 커리-하워드 대응(Curry-Howard Correspondence)과 크라이젤의 수정된 실현 가능성(Kreisel’s Modified Realizability) 해석을 사용하여, 구성된 증명으로부터 검증된(Certified) 함수형 프로그램을 자동으로 추출한다. 추출된 결과물은 주로 Scheme이나 Haskell 코드로 변환할 수 있다.
-
구현 환경 시스템 자체는 함수형 프로그래밍 언어인 Scheme으로 작성되었으며, 사용자는 주로 GNU Emacs 인터페이스(Proof General 등)를 통해 시스템과 상호작용한다.
-
항 재작성 (Term Rewriting) 정규화(Normalization by Evaluation, NbE) 기법을 적극 활용하여 계산적인 증명 과정을 자동화하고 단순화한다.
주요 정리 증명기 비교
Minlog의 위치를 파악하기 위해 다른 서구권의 주요 정리 증명기(Coq, Isabelle/HOL)와 비교하면 다음과 같다.
| 비교 항목 | Minlog | Coq | Isabelle/HOL |
|---|---|---|---|
| 개발 기관 | 독일 뮌헨 대학교 (LMU Munich) | 프랑스 국립 정보학 자동화 연구소 (INRIA) | 영국 케임브리지 대학교 & 독일 뮌헨 공과대학교 (TUM) |
| 기반 논리 | 최소 논리 (Minimal Logic) 및 유한 타입 | 귀납적 구축 계산법 (Calculus of Inductive Constructions) | 고차 논리 (Higher-Order Logic) |
| 구현 언어 | Scheme | OCaml | Standard ML / Scala |
| 핵심 강점 | 증명으로부터의 순수 알고리즘 추출 및 계산적 분석 | 프로그램 검증 및 형식 수학 (Formal Mathematics) | 대규모 증명 자동화 및 시스템 검증 |
| 추출 대상 언어 | Scheme, Haskell | OCaml, Haskell, Scheme | SML, OCaml, Haskell, Scala |
출처 (Sources)
- Schwichtenberg, H., & Wainer, S. S. (2011). Proofs and Computations. Cambridge University Press. (영국 케임브리지 대학교 출판부)
- LMU Munich Logic Group. The Minlog System. Ludwig-Maximilians-Universität München. (독일 뮌헨 대학교 공식 문서:
http://www.mathematik.uni-muenchen.de/~logik/minlog/) - Wiedijk, F. (Ed.). (2006). The Seventeen Provers of the World (Lecture Notes in Computer Science, Vol. 3600). Springer-Verlag Berlin Heidelberg. (독일 슈프링어 출판사)