자동 추리

Automated reasoning

컴퓨터 과학, 특히 지식 표현과 추론 그리고 금속학에서, 자동 추론의 영역은 추론의 다른 측면을 이해하는 데 전념합니다.자동 추론의 연구는 컴퓨터가 완전히 또는 거의 자동으로 추론을 할 수 있도록 하는 컴퓨터 프로그램을 제작하는 데 도움이 됩니다.자동화된 추론은 인공지능의 하위 분야로 여겨지지만, 이론적인 컴퓨터 공학 및 철학과도 관련이 있다.

자동 추론의 가장 발전된 하위 영역은 자동화된 정리 증명(및 덜 자동화되었지만 보다 실용적인 대화형 정리 증명 하위 분야)과 자동화된 증명 확인(고정된 [citation needed]가정 하에서 보장된 올바른 추리로 간주됨)입니다.유도와 [1]유괴를 이용한 유추에 의한 추리 작업도 광범위하게 행해졌다.

다른 중요한 주제로는 불확실성 하에서의 추론과 비단조적 추론이 있다.불확실성 필드의 중요한 부분은 논의이며, 여기서 보다 표준적인 자동 연산에 더해 최소성과 일관성의 추가 제약이 적용된다.John Pollock의 OSCAR[2] 시스템은 단순한 자동화된 정리 검증 시스템보다 더 구체적인 자동화된 논쟁 시스템의 한 예입니다.

자동화된 추론의 도구와 기술은 고전적인 논리학과 계산, 퍼지 논리, 베이지안 추론, 최대 엔트로피와 훨씬 덜 형식적인 애드혹 기술을 포함한다.

초년

형식논리의 발달은 인공지능의 발달로 이어진 자동추론의 분야에서 큰 역할을 했다.형식적 증명은 모든 논리적 추론이 수학의 기본 공리에 대해 다시 확인되었다는 증거이다.모든 중간 논리 단계가 예외 없이 제공됩니다.직감에서 논리로의 번역이 일상적이라고 해도 직감에는 호소할 수 없다.따라서 공식적인 증명은 덜 직관적이고 논리적 [3]오류에 덜 취약하다.

어떤 사람들은 많은 논리학자들과 컴퓨터 과학자들이 모인 1957년의 코넬 여름 회의를 자동화된 추리 혹은 자동화된 [4]추론의 기원으로 여긴다.다른 사람들은 그것이 1955년 뉴웰, 쇼, 사이먼의 논리 이론가 프로그램이나 마틴 데이비스가 1954년 프레스버거의 결정 절차를 시행하면서 [5]시작됐다고 말한다.

자동 추론은 중요하고 인기 있는 연구 영역이지만, 80년대와 90년대 초에 "AI 겨울"을 거쳤다.하지만 그 후 그 분야는 다시 살아났다.예를 들어 2005년 마이크로소프트는 사내 프로젝트의 많은 부분에서 검증 기술을 사용하기 시작했으며 2012년 버전의 Visual [4]C에 논리 사양과 체크 언어를 포함할 예정입니다.

중요한 공헌

프린키피아 매스매티카는 알프레드 노스 화이트헤드와 버트랜드 러셀이 쓴 형식 논리학의 획기적인 작품이다.수학의 원리를 의미하는 프린키피아 매스매티카는 상징 논리학의 관점에서 수학 표현식의 전부 또는 일부를 도출하기 위한 목적으로 쓰여졌다.프린키피아 매스매티카는 1910년, 1912년, [6]1913년에 세 권으로 처음 출판되었다.

논리이론가(LT)는 1956년 앨런 뉴웰, 클리프 쇼, 허버트 A에 의해 개발된 최초의 프로그램이다. Simon은 이론을 증명하는데 있어서 "인간 논리를 모방"했고, Principia Mathematica의 제2장에서 52개의 이론에서 입증되었고, 그 [7]중 38개를 증명했다.이 프로그램은 이론들을 증명하는 것 외에도 화이트헤드와 러셀이 제공한 것보다 더 우아한 이론들 중 하나에 대한 증거를 찾아냈다.결과를 발표하려다 실패한 후 Newell, Shaw 및 Herbert는 1958년 The Next Advance in Operation Research를 발표했습니다.

"이제 세상에는 생각하고, 배우고, 창조하는 기계가 있습니다.게다가, 이러한 일을 할 수 있는 그들의 능력은 인간의 정신이 적용된 범위와 함께 광범위하게 다뤄질 때까지 빠르게 증가할 것이다."[8]

형식 교정 예시

연도 정리 프루프 시스템 포멀라이저 종래의 실증
1986 첫 번째 불완전성 보이어무어 샹카루[9] 괴델
1990 이차상호성 보이어무어 러시노프[10] 아이젠슈타인
1996 미적분의 기초 홀 라이트 해리슨 헨스톡
2000 대수학의 기초 미자르 밀레우스키 브린스키
2000 대수학의 기초 동작 Geuvers 등 크네세르
2004 4색 동작 곤티에 로버트슨 외
2004 소수점 이사벨 아비가드 등 셀버그-에르데시스
2005 조던 곡선 홀 라이트 헤일즈 토마센
2005 브루어 고정점 홀 라이트 해리슨 쿤
2006 플라이스펙 1 이사벨 바우어닙코우 헤일즈
2007 코시 잔여물 홀 라이트 해리슨 고전적인
2008 소수점 홀 라이트 해리슨 분석 증명
2012 페이트톰슨 동작 곤티에 [11]외 벤더, 글라우버만, 피터팔비
2016 부울 피타고라스 3배 문제 SAT로 정식화 훌레 [12]등 없음.

실증 시스템

보이어-무어 정리 프로버(NQTHM)
NQTHM의 디자인은 John McCarthy와 Woody Bledsoe의 영향을 받았다.1971년 스코틀랜드 에딘버러에서 시작된 이 정리는 순수 리스프를 사용하여 제작된 완전 자동 정리법입니다.NQTHM의 주요 측면은 다음과 같습니다.
  1. 동작 로직으로서의 리스프 사용.
  2. 전체 재귀 함수에 대한 정의 원리에 대한 의존.
  3. 개서 및 "평가"의 광범위한 사용.
  4. 유도 휴리스틱은 상징적 [13]평가의 실패에 기초한다.
홀 라이트
OCaml로 작성된 HOL Light는 단순하고 깨끗한 논리 기반과 깔끔한 구현을 제공하도록 설계되었습니다.이것은 본질적으로 고전적인 고차 [14]논리의 또 다른 증명 보조 도구입니다.
동작
프랑스에서 개발된 Coq는 Objective CAML 또는 Haskell 소스 코드 중 하나로 사양에서 실행 가능한 프로그램을 자동으로 추출할 수 있는 또 다른 자동화된 증명 도우미입니다.속성, 프로그램 및 증명은 귀납적 구성 미적분([15]CIC)이라고 불리는 동일한 언어로 공식화됩니다.

적용들

자동화된 추론은 자동화된 정리 프로버를 구축하기 위해 가장 일반적으로 사용되어 왔다.하지만, 종종 정리론자들은 효과적이기 위해 인간의 지침을 필요로 하고 그래서 더 일반적으로 증명 보조자로서의 자격을 갖습니다.어떤 경우에는 그러한 증명자들이 정리를 증명하기 위한 새로운 접근법을 생각해냈다.논리 이론가는 이것의 좋은 예이다.이 프로그램은 프린키피아 매스매티카에서 화이트헤드와 러셀이 제공한 증명보다 더 효율적인 이론 중 하나를 제시했습니다.형식 논리, 수학 및 컴퓨터 과학, 논리 프로그래밍, 소프트웨어 및 하드웨어 검증, 회로 설계 등의 문제를 해결하기 위해 자동 추론 프로그램이 적용되고 있습니다.TPTP(Sutcliffe and Suttner 1998)는 정기적으로 업데이트되는 이러한 문제의 라이브러리입니다.또한 CADE 회의(Pelletier, Sutcliffe 및 Suttner 2002)에서 정기적으로 개최되는 자동 정리 프로버 간의 경쟁도 있다. 경쟁에 대한 문제는 TPTP [16]라이브러리에서 선택된다.

「 」를 참조해 주세요.

회의 및 워크숍

일지

커뮤니티

레퍼런스

  1. ^ 드푸르노, 길레스, 니콜라스 펠티에."자동 추리에서의 아날로그 및 납치"IJCAI (1) 1997.
  2. ^ 존 L. 폴록
  3. ^ C. Hales, Thomas "Formal Proof", 피츠버그 대학교2010년 10월 19일 취득
  4. ^ a b 자동 공제(AD), [PRL 프로젝트의 성격]2010년 10월 19일 취득
  5. ^ Martin Davis (1983). "The Prehistory and Early History of Automated Deduction". In Jörg Siekmann; G. Wrightson (eds.). Automation of Reasoning (1) — Classical Papers on Computational Logic 1957–1966. Heidelberg: Springer. pp. 1–28. ISBN 978-3-642-81954-4. 여기: 페이지 15
  6. ^ 스탠포드 대학의 '프린키피아 매스매티카'입니다.2010-10-19 취득
  7. ^ "논리 이론가와 그 아이들"2010-10-18 취득
  8. ^ SRI International 컴퓨터 과학 연구소, 나타라잔 리틀 엔진 오브 프루프2010-10-19 취득
  9. ^ Shankar, N. (1994), Metamathematics, Machines, and Gödel's Proof, Cambridge, UK: Cambridge University Press, ISBN 9780521585330
  10. ^ Russinoff, David M. (1992), "A Mechanical Proof of Quadratic Reciprocity", J. Autom. Reason., 8 (1): 3–21, doi:10.1007/BF00263446
  11. ^ Gonthier, G.; et al. (2013), "A Machine-Checked Proof of the Odd Order Theorem" (PDF), in Blazy, S.; Paulin-Mohring, C.; Pichardie, D. (eds.), Interactive Theorem Proving, Lecture Notes in Computer Science, vol. 7998, pp. 163–179, doi:10.1007/978-3-642-39634-2_14, ISBN 978-3-642-39633-5
  12. ^ Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016). "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer". Theory and Applications of Satisfiability Testing – SAT 2016. Lecture Notes in Computer Science. Vol. 9710. pp. 228–245. arXiv:1605.00723. doi:10.1007/978-3-319-40970-2_15. ISBN 978-3-319-40969-6.
  13. ^ 보이어-무어 정리 프로버.2010년 10월 23일
  14. ^ Harrison, John HOL Light: 개요.2010-10-23 취득
  15. ^ Coq의 개요2010-10-23 취득
  16. ^ 자동 추리, 스탠포드 백과사전2010-10-10 취득

외부 링크