Logic  Theorist

 

1955 년에 Allen Newell, J.C. Shaw, Herbert Simon최초의  AI 프로그램 Logic Theorist (LT) 를 선보였다. (Carnegie Institute of Technology, 지금의 Carnegie Mellon 대학). 그것은 수학 문제를 풀기위한 것이며 추론 프로그램으로서 비수치적으로 사고하는 컴퓨터 프로그램이라고 소개하였다. 그것은 검색 (searching), 목표지향 행동 (goal-oriented behavior), 규칙의 응용 (application of rules) 을 복합하여 사용한 정리를 증명했다 (정리증명 (Theorem Proving)). 그것은 IPL 언어로 리스트 처리 기술 (list processing technique) 을 사용하여 만든 것이다. 프로그램은 여러 방송 매체를 통해 소개되기도 하였다. . ..

1955 년에 Allen Newell, Herbert Simon, J.C. Shaw 이 최초의 AI 언어 "IPL (Information Processing Language)" 을 만들었다. 그것은 Logic Theorist 를 만들기 위해 개발한 새로운 컴퓨터 언어이다. 그것은 associative memory 를 흉내내어 관련된 정보의 조각들 사이에 포인터를 제공하며, 상호작용하는 기호 (Symbol) 구조를 생성, 변화, 파괴하는 기능이 제공되었다.

인공지능 (Artificial Intelligence) 가 처음 탄생한 1956 년 여름 Dartmouth 에서의 워크샵에서 Simon 은 "우리는 비수치적으로 사고할 수 있는 컴퓨터 프로그램을 발명했으며, 그것으로 캐캐묵은 심신문제 (Mind-Body Problem) 를 해결할 수 있다" 고 주장하였다. 그 워크샵 직후에 그 프로그램은 Russell 과 Whitehead 의 수학원리 (Principia Mathematica) 의 2 장에 있는 대부분의 정리를 증명할 수 있었다.  Simon 이 Russell 에게 그 프로그램으로 하나의 정리를 위한 증명을 할 때 Principia 에서 보다도 더 짧게 증명하는 것을 보여주었고 Russell 은 기뻐했다고 전해진다. Journal of Symbolic Logic 편집자는 그리 큰 인상을 받지 못했고, Newell 과 Simon 공저의 저술과 Logic Theorist 의 출간을 거절했다. ....... (Wikipedia : Logic Theorist)

..... 기호 논리로 정리를 증명할 수 있도록 프로그램된 컴퓨터 ..... 논리의 순열과 조화가 복잡하므로, 모든 확률을 조사하여 문제점을 해결하는 것은 극히 간단한 상황에서만 실질적이다. 지름길을 택하는 것이 실제적으로 유리하다 (발견적 방법, 휴리스틱 (Heuristic)). 이런 것들은 해결책을 보장하지는 않으나 어느 타당한 시기에 발견될 수 있는 가능성을 갖고 있다.

여기서 서술된 정리를 증명할 수 있는 프로그램은, 발견적 지도법이 컴퓨터 내에서 어떻게 사용되는가를 보여주기 위해 뉴웰과 쇼와 사이몬이 고안하였다. 그들은 그것을 논리적 정리를 위한 컴퓨터라고 하며 약자로 "LT" 라 칭한다. 그들은 시험 결과로 『수학원리 (Principia Mathematica)』의 제 2 장에서 52 개의 정리를 선택했다. 그리고 정리를 증명하기 위해 그 책에서 5 개의 공리와 3 개의 추론을 컴퓨터 기억장치에 수록했고, 컴퓨터의 기억장치를 조사하고 기호를 작동하여 컴퓨터를 만들었다. 그 정리는 발표한 순서로 기계에 보내진다. 기계에 의해 프로그램이 증명된 후 각 정리가 저장되도록 되어 있다. "증명된 정리" 는 다음의 정리를 증명하는 데 사용된다. ... (정리를 증명하는 기계 : Donald G. Fink )

site :

Wikipedia : Logic Theorist

video :

AI and The Logic Theorist : 2009/02/04