Gerhard
Gentzen
(독일 수학자 논리학자 1909~1945)
Gerhard Gentzen 은 독일에서 태어나 체코의 프라하
포로수용소에서 러시아인에 의해 나찌에 충성한 경력으로 체포되어 죽었다.
1929 에서 1933 년까지 University of Göttingen
에 있으면서 주로 foundations of mathematics, in proof theory, specifically natural deduction
and the sequent
calculus 를 연구했다. 그의 cut-elimination theorem 은 proof-theoretic semantics
의 이정표가 되었으며, 그의 "Investigations into Logical Deduction"
에 대한 철학적 언급은 Wittgenstein 의 금언 "meaning is use" 와 함께
inferential role semantics 을 위한 출발점이 되었다. ................ (Wikipedia
: Gerhard Gentzen)
term :
논리학
(Logic) 수학
(Mathematics) 연역법
(Deduction) 의미론
(Semantics) Ludwig Wittgenstein
Gerhard Gentzen
paper :
- Untersuchungen über das logische Schliessen.
Mathematische Zeitschrift, 1934
- Gentzens Problem: Mathematische Logik im
nationalsozialistischen Deutschland. Eckart Menzler-Trott. Birkhäuser Verlag, 2001
- Collected Papers of Gerhard Gentzen. M. E. Szabo. North-Holland,
1969.
site :
- Gerhard
Gentzen : St
Andrews
- 구조 로직(constructive logic)의 이해: 증명 시스템과 람다 계산법(lambda calculi)에 대하여
: Constructive logics Part I: A tutorial on proof systems and
typed lambda-calculi, Jean
Gallier, TCS 110, 1993
....... 수학에서 연구하던 논리(logic)를 프로그래밍 언어에 적용하는 (현재 활발하게 연구되고 있는) 연구
분야를 이해하기 위하여, 그 배경이 되는 구조 논리(constructive logic)를 살펴 본다. 이미, 이전의 세미나(judaigi)에서
발표하였고, 또한 배민오 박사님 세미나에서 깊게 다루었지만, 위의 발표 논문을 토대로 한번 더 살펴 본다. 자연
추론법(natural deduction)에 의한 구조 논리 증명 시스템과 Gentzen의 귀추 계산법(sequent calculi)에 의한 구조
논리 증명 시스템이 증명할 수 있는 범위가 같음을 보인다. (자연 추론법에 비해 귀추 계산법은 증명을 자동화하기가 쉽다.) 이를 위하여 자연
추론법의 모든 증명에 표준형(normal form)이 있음을 보이고, 자연 추론법의 증명을 귀추 계산법 + (cut) 규칙의 증명으로 바꾸는
알고리즘 N 과 귀추 계산법을 자연 추론법의 표준형 증명으로 바꾸는 알고리즘 G 를 제시한다. 마지막으로
Gentzen의 cut 규칙 제거 정리를 통해, 자연 추론법의 증명과 귀추 계산법이 상호 변환 가능함을 보인다. .....