의견.png

"자동추론"의 두 판 사이의 차이

해시넷
이동: 둘러보기, 검색
(자동 추론의 논리적 기초)
7번째 줄: 7번째 줄:
  
 
==첫 구현==
 
==첫 구현==
 +
제2차 세계대전 직후, 최초의 [[범용 컴퓨터]](general purpose computer)가 보급되었다. 1954년, 마틴 데이비스(Martin Davis)는 [[프린스턴 고등연구소]](Princeton Institute)에서 [[JOHNICA]] 진공관 컴퓨터를 위한  [[Presburger]]의 알고리즘을 프로그래밍(programming) 했다.
 +
 
==문제의 결정 가능성==
 
==문제의 결정 가능성==
 
==관련문제==
 
==관련문제==

2020년 7월 17일 (금) 13:28 판

자동 추론은 컴퓨터 프로그램에 의한 수학적 이론의 증명 문제를 다루는 자동화된 추론과 수학 논리(logic)의 하위 분야다. 수학적 증거에 대한 자동화된 추론은 컴퓨터 과학의 발전에 주요한 자극제였다. 인공지능(AI) 연구에 있어 핵심이기도 하다.[1]

자동 추론의 논리적 기초

19세기 말과 20세기 초의 논리는 현대 논리와 정형화(formalised)된 수학의 발달이 이었다. 1879년, 고틀로프 프레게(Gottlob Frege)는 자신의 저서 베그리프시크리프트(Begriffsschrift)에서 '완전한 명제로 이뤄진 미적분'과 '근본적인 현대 논리'를 모두 소개했다. 1884년엔 수학을 형식 논리로 표현한 산술 기초(Foundations of Arithmetic)를 출간했다. 이러한 접근은 러셀(Russell Bertrand)과 화이트헤드(Whitehead Alfred North)가 1910~1913년에 처음 출간한 수학 원리(Principia Mathematica)에 큰 영향을 주었다. 그 뒤로도 1927년에 개정된 수학 원리로 접근을 시도했다. 러셀과 화이트헤드는 사회에서 두루 통하는 진리나 도리인 '공리'와 형식논리의 '추론규칙'을 사용해서 수학적인 진리를 도출할 수 있다고 생각했고, 이로 인해 '자동화'란 것에 접근할 수 있게 된다. 1929년, 모히제스 프레스버거(Mojżesz Presburger)는 덧셈과 등호가 있는 자연수 이론(현, 프레스버거 산술(Presburger arithmetic))을 해독할 수 있다는 것을 보여주고, 그 언어에서 주어진 문장이 참인지 거짓인지를 판단할 수 있는 알고리즘을 주었다.

그러나, 이런 좋은 결과가 나온 직후, 1931년에 커트 괴델(Kurt Gödel)은 '프린키니아 매스매티카 및 관련 시스템의 확인되지 않은 문제들에 대하여(On Formally Undecidable Propositions of Principia Mathematica and Related Systems)'를 발표하여, 충분히 자명론 시스템에는 증명할 수 없는 참된 진술들이 있음을 보여주었다. 이 주장은 1930년대에 알론조 처치(Alonzo Church)와 앨런 튜링에 의해 더욱 발전하게 된다.[1]

첫 구현

제2차 세계대전 직후, 최초의 범용 컴퓨터(general purpose computer)가 보급되었다. 1954년, 마틴 데이비스(Martin Davis)는 프린스턴 고등연구소(Princeton Institute)에서 JOHNICA 진공관 컴퓨터를 위한 Presburger의 알고리즘을 프로그래밍(programming) 했다.

문제의 결정 가능성

관련문제

산업용

1차 정리 증명

벤치 마크, 경쟁 및 소스

인기있는 기술

소프트웨어 시스템

자유 소프트웨어

독점 소프트웨어

각주

각주

참고자료

  의견.png 이 자동추론 문서는 인공지능 기술에 관한 토막글입니다. 위키 문서는 누구든지 자유롭게 편집할 수 있습니다. [편집]을 눌러 이 문서의 내용을 채워주세요.