predicate calculus를 이용하는 언어로 "PROLOG"라는 언어가 있습니다. 제가 제일 좋아하는 프로그래밍 언어인데 사장되어 가는 분위기죠 이 언어를 이용하면 매우 쉽게 theorem prover를 만들 수 있습니다. 사실 이 언어 자체가 일종의 theorem prover죠. '추론'이라는 과정과 theorem prover는 분명 밀접한 연관관계가 있기 때문에 인공지능분야에서 이 부분을 아주 심도있게 연구하는 분야가 있습니다. 하지만 그 결과는 그다지 밝지 못한 상태입니다. 현재의 상태의 theorem prover는 매우 초보적이고 단순한 결과밖에 만들지 못한다는 것이 밝혀져 있습니다. predicate logic에서 가장 단순한 것이 first-order predicate logic입니다. 환상님이 말씀하신 시중의 프로그램들은 현재 여기에서 벗어나지 못하고 있는 것들입니다. 사람은 추론을 할때 매우 추상적인 상황까지 추론에 이용합니다. 즉, 추론을 할때 이용하는 "추론규칙"이나 추론을 행하고 있는 주체(즉 자기 자신)까지 추론의 상황에 이용하는 것입니다. 이러한 것은 second-order predicate login에 해당하는 것이고 나아가 무한-order predicate logic까지 가능하게 되는데 궁극적인 추론을 가능케 하려먼 무한-order까지 해나가야만 합니다. 여기쯤 오면 괴델의 "불완정성 정리"가 등장해서 이러한 것들이 불가능하기 때문에 인공지능이란 불가능 하다라고 주장을 사람들이 판을 치게 되는데, 제 생각으로는 사람의 추론과정은 결코 무한-order까지 하는 것이 하니고 "적당한" 곳까지 임의로 프로세스를 진행시킨다고 보므로 괴델의 이론까지 들먹여 가면서 인공지능이 불가능하다고 주장하는 사람들의 의견에는 동의할 수 없다고 봅니다. 그럼 다시 처음의 문제로 돌아가서 "자동프로그램생성기" 문제를 마지막으로 집고 넘어가죠. 이 문제는 근본적으로 theorem prover와 같은 배경을 가지고 있습니다. 수학적으로나 어떤 형태로든 주어진 spec에 따라 그 기능을 수행하는 프로그램을 생성하는 일은, 주어진 공리체계에 따라 theorem을 생성하거나 증명하는 문제와 근본적으로 같습니다. 그럼 이러한 자동프로그램 생성기의 한계는 불을 보듯 뻔한 것이죠 너무 쉽게 문제를 풀면 first-order에 해당하는 유치한 것들만 가능하게 되고 더 앞으로 나아가자니 괴델의 정리가 앞을 막고 있습니다. 그 중간을 적당히 해나가는 것이 바로 인공지능인데 환상님의 꿈꾸는 그 자동프로그램생성기를 제대로 만드는 일은 인공지능기계를 만드는 일과 결국 같은 일이 될것이라는 것이 제 생각입니다. __ 쇼팽