오토매트

오토매트(Automating Math)는 포함된 자동화된 증명 검사자가 정확성을 검증할 수 있는 방식으로 완전한 수학 이론을 표현하기 위해 1967년부터 니콜라스 고베르 드 브루이진이 고안한 공식 언어다.

개요

오토매트 시스템은 후에 채택되거나 활자화된 람다 미적분학 및 명시적 대체와 같은 분야에서 재창조된 많은 새로운 개념들을 포함했다.종속형은 대표적인 예다.오토마트는 또한 커리-하워드의 통신을 이용한 최초의 실용적인 시스템이었다.명제는 증거의 집합("범주"라고 불림)으로 표현되었고, 검증의 문제는 비빈(유형 거주)의 문제가 되었고, 드 브루이진은 하워드의 작품을 알지 못했으며, 서신을 독자적으로 진술하였다.^[1]

L. S. 반 벤트헴 주팅은 1976년 이 박사 논문의 일부로서 에드먼드 랜도의 분석기반을 오토마트로 번역하고 그 정확성을 점검했다.

그러나 오토마스는 그 당시에 널리 알려진 적이 없었고, 그래서 널리 쓰이지 못했다; 그럼에도 불구하고, 그것은 논리적 프레임워크와 증명 보조자의 후기 개발에 큰 영향을 끼쳤다.^[2][3]아직 활발하게 사용되고 있는 정형화된 수학을 쓰고 체크하는 시스템인 미자르 제도는 오토마스의 영향을 받았다.

참고 항목

• QED 선언문

참조

외부 링크

• 자동 경로 아카이브(미러)
• 오토매트 35주년을 기념하는 워크샵의 35년 오토매트 홈페이지
• Freek Wiedijk별 오토매트 페이지