미니로그
MINLOGMINLOG는 Helmut Schwichtenberg 팀에 의해 뮌헨 대학에서 개발된 증명 보조 도구입니다.
MINLOG는 1차 자연감산 미적분에 기초한다.이것은 고전적이거나 직관적인 논리가 아닌 최소한의 논리만을 사용하여 계산 가능한 함수에 대해 추론하기 위한 것입니다.MINLOG의 배후에 있는 주된 동기는 프로그램 개발 및 프로그램 검증을 위해 Proofs-as-Programs 패러다임을 이용하는 것입니다.사실 증명은 정규화할 수 있는 1등급 물체로 취급됩니다.만약 공식이 존재한다면, 그 증명은 그것의 인스턴스를 읽어내거나 증명 변환에 의해 프로그램 개발에 적절하게 변경될 수 있다.이를 위해 MINLOG는 증명 용어에서 직접 기능 프로그램을 추출할 수 있는 도구를 갖추고 있습니다.이것은 또한 정교한 A-번역을 사용하여 비건설적 증거에도 적용된다.효율적인 용어 개서 장치로 평가하여 자동 증명 검색 및 정규화를 지원합니다.
