자동 정리 증명

Automated theorem proving

자동 정리 증명(ATP 또는 자동 추리라고도 함)은 컴퓨터 프로그램에 의한 수학 정리의 증명에 관한 자동화된 추론 및 수학적 논리의 하위 분야입니다.수학적 증명에 대한 자동화된 추론은 컴퓨터 과학 발전에 큰 자극제가 되었다.

논리적 기초

형식화된 논리의 뿌리는 아리스토텔레스에게 거슬러 올라가는 반면, 19세기 말과 20세기 초는 현대 논리와 형식화된 수학의 발전을 보았다.프레게의 Begriffsschrift (1879)는 완전한 명제 미적분과 본질적으로 현대 술어 [1]논리학을 둘 다 도입했다.1884년에 [2]출판된 그의 산술 기초는 수학을 형식 논리로 표현했다.이 접근법은 러셀과 화이트헤드가 [3]1910-1913년에 처음 출판한 영향력 있는 프린키피아 매스매티카에서 1927년에 [4]개정된 제2판을 통해 계속되었다.러셀과 화이트헤드는 원칙적으로 자동화의 과정을 열어주는 형식 논리의 공리와 추론 규칙을 사용하여 모든 수학적 진실을 도출할 수 있다고 생각했습니다.1920년, 토랄프 스콜렘은 레오폴트 뢰벤하임의 이전 결과를 단순화하여, 뢰벤하임-스콜렘 정리로 이어졌고, 1930년에는 헤르브란트 우주의 개념과 헤르브란트 해석으로 이어져 1차 공식의 (그리고 정리의 타당성)을 (무한히 많은 것으로 줄였다.만족도 문제.[5]

1929년, Mojesesz Presburger는 덧셈과 등식을 수반하는 자연수 이론이 결정 가능하다는 것을 보여주었고, 언어의 주어진 문장이 참인지 [6][7]거짓인지를 결정할 수 있는 알고리즘을 주었다.그러나, 이 긍정적인 결과 직후에, Kurt Gödel은 충분히 강한 공리 체계에는 시스템에서 증명될 수 없는 진실된 진술이 있다는 것을 보여주는 "공식적으로 결정 불가능한 명제에 대하여"를 출판했다.이 주제는 1930년대에 Alonzo Church와 Alan Turing에 의해 더욱 발전되었는데, 그는 한편으로는 계산 가능성의 두 가지 독립적이지만 동등한 정의를 제공하고, 다른 한편으로는 결정 불가능한 질문에 대한 구체적인 예를 제시하였다.

첫 번째 구현

제2차 세계대전 직후, 최초의 범용 컴퓨터가 사용 가능하게 되었다.1954년 마틴 데이비스는 뉴저지 프린스턴 고등연구소에서 JONNIAC 진공관 컴퓨터에 대한 Presburger의 알고리즘을 프로그래밍했습니다.데이비스는 "그것의 위대한 승리는 짝수 두 개의 [7][8]합이 짝수라는 것을 증명하는 것이었다"고 말했다.더 야심찬 것은 1956년 앨런 뉴웰, 허버트 A에 의해 개발된 프린키피아 매스매티카의 명제 논리에 대한 추론 시스템인 논리 이론 기계이다. 사이먼과 J.C. 쇼. 또한 JOHNIAC에서 작동하는 논리 이론 기계는 작은 일련의 명제 공리와 세 가지 추론 규칙으로부터 증거를 구성했습니다: 모더스 포넨, (명제) 변수 치환, 그리고 그들의 정의에 의한 공식의 치환.이 시스템은 발견적 지침을 사용했고 프린키피아 [7]최초의 52개 이론 중 38개를 증명하는데 성공했다.

논리 이론 기계의 "휴리스틱" 접근법은 인간 수학자들을 모방하려고 노력했고, 모든 유효한 정리에 대한 증거를 찾을 수 있다는 것을 원칙적으로도 보장하지 못했다.이와는 대조적으로, 다른 보다 체계적인 알고리즘은 적어도 이론적으로는 1차 로직의 완전성을 달성했습니다.초기 접근법은 헤르브란트와 스콜렘의 결과에 의존하여 헤르브란드 우주의 항으로 변수를 인스턴스화함으로써 1차 공식을 연속적으로 더 큰 명제 공식 세트로 변환했습니다.그런 다음 여러 가지 방법을 사용하여 명제 공식의 만족도를 확인할 수 있습니다.길모어의 프로그램은 공식의 만족도가 분명한 형태인 [7][9]분리 정규형으로의 변환을 사용했다.

문제의 결정 가능성

기본 논리에 따라, 공식의 타당성을 결정하는 문제는 사소한 것에서 불가능한 것까지 다양합니다.명제 논리의 빈번한 경우, 문제는 결정 가능하지만 co-NP-완전이며, 따라서 일반적인 증명 작업에 대해 지수 시간 알고리즘만이 존재하는 것으로 여겨진다.1차 술어 미적분학의 경우, 괴델의 완전성 정리는 논리적으로 유효한 공식(증명 가능한 진술)이 정확히 유효하다는 것을 말한다. 따라서 유효한 공식을 확인하는 것은 반복적으로 열거할 수 있다: 무한한 자원이 주어지면, 어떤 유효한 공식도 결국 증명될 수 있다.그러나 잘못된 공식(특정 이론에 의해 수반되지 않는 공식)이 항상 인식될 수는 없습니다.

위의 내용은 페아노 산술과 같은 1차 이론에도 적용된다.그러나 1차 이론에 의해 기술될 수 있는 특정 모델의 경우, 일부 진술은 참일 수 있지만 모델을 기술하기 위해 사용되는 이론에서는 결정할 수 없습니다.예를 들어, 괴델의 불완전성 정리에 의해, 우리는 자연수에 대한 적절한 공리가 참인 이론이 비록 적절한 공리의 목록이 무한히 열거될 수 있도록 허용된다 하더라도 자연수에 대한 모든 1차 진술이 참이라는 것을 증명할 수 없다는 것을 안다.따라서 자동정리프로버는 조사되는 진술이 사용되는 이론에서 결정되지 않을 때, 비록 그것이 관심 모델에서 사실일지라도 증거를 정확하게 찾는 동안 종료되지 않을 것이다.이러한 이론적 한계에도 불구하고, 실제로, 정리론자들은 심지어 어떤 1차 이론(정수와 같은)에 의해 완전히 묘사되지 않은 모형에서도 많은 어려운 문제들을 풀 수 있다.

관련 문제

더 간단하지만 관련이 있는 문제는 증명 검증이며, 여기서 정리에 대한 기존 증명은 유효하다고 증명됩니다.이를 위해서는 일반적으로 각각의 개별 증명 단계를 원시 재귀 함수 또는 프로그램에 의해 검증할 수 있어야 하며, 따라서 이 문제는 항상 결정될 수 있다.

자동화된 정리프로버에 의해 생성되는 증명은 전형적으로 매우 크기 때문에 증명압축의 문제는 매우 중요하며, 증명프로버의 출력을 더 작게 만들고 결과적으로 더 쉽게 이해하고 확인할 수 있도록 하기 위한 다양한 기술이 개발되어 왔다.

교정 보조자는 시스템에 힌트를 줄 수 있는 사람이 필요합니다.자동화 정도에 따라 프로버는 기본적으로 프루프 체커로 축소되어 사용자가 정식으로 프루프 체커를 제공하거나 중요한 프루프 태스크를 자동으로 실행할 수 있다.인터랙티브 프로버는 다양한 작업에 사용되지만, 완전 자동 시스템조차도 적어도 오랜 시간 동안 인간 수학자들을 따돌린 것, 즉 로빈스 [10][11]추측을 포함한 많은 흥미롭고 어려운 이론이 입증되었습니다.그러나 이러한 성공은 산발적이며, 어려운 문제를 해결하려면 보통 숙련된 사용자가 필요합니다.

정리 증명과 다른 기술 사이에 또 다른 구별이 생기기도 하는데, 여기서 프로세스는 공리에서 시작하여 추론 규칙을 사용하여 새로운 추론 단계를 생성하는 전통적인 증명으로 구성되는지 여부를 증명하는 것으로 간주됩니다.다른 기술로는 모델체크를 들 수 있는데, 가장 단순한 경우에서는 많은 가능한 상태의 브루트포스 열거가 포함됩니다(모델체커의 실제 실장은 매우 영리함을 필요로 하며 단순히 브루트포스(bretforce)로 축소되지 않습니다).

모델 체크를 추론 규칙으로 사용하는 하이브리드 정리 증명 시스템이 있습니다.또한 특정 정리를 증명하기 위해 작성된 프로그램도 있는데, 만약 그 프로그램이 특정한 결과로 끝난다면, 그 정리가 참이라는 (일반적으로 비공식적인) 증거를 가지고 있다.이것의 좋은 예는 4색 정리에 대한 기계 보조 증명이었는데, 이것은 프로그램의 엄청난 계산 크기 때문에 인간에 의해 본질적으로 검증이 불가능했던 최초의 주장된 수학적 증명으로서 매우 논란이 되었다.프로그램 지원 증명의 또 다른 예는 Connect Four 게임이 항상 첫 번째 플레이어가 이길 수 있다는 것을 보여주는 것이다.

산업용도

자동 정리 증명의 상업적인 사용은 대부분 집적회로 설계와 검증에 집중되어 있다.Pentium FDIV 버그 이후, 현대의 마이크로프로세서의 복잡한 부동소수점 유닛은, 한층 더 정밀하게 설계되고 있습니다.AMD, Intel 및 기타 제품은 프로세서 내에서 분할 및 기타 작업이 올바르게 구현되었는지 검증하기 위해 자동화된 정리를 사용합니다.

1차 정리 증명

1960년대 후반, 기관들은 자동 공제 연구에 자금을 대면서 실용적인 적용의 필요성을 강조하기 시작했다.최초의 성과 영역 중 하나는 파스칼, 아다 등의 언어로 된 컴퓨터 프로그램의 정확성을 검증하는 문제에 1차 정리 검증자를 적용한 프로그램 검증이었다.초기 프로그램 검증 시스템 중 주목할 만한 것은 스탠포드 [12][13][14]대학의 데이비드 러컴이 개발한 스탠포드 파스칼 검증 시스템입니다.이것은 스탠포드 해상도 프로버도 존 앨런 로빈슨의 해상도 원리를 사용하여 스탠포드에서 개발한 해상도 프로버에 기초하고 있다.이것은 해답이 공식적으로 [citation needed]발표되기 전에 미국 수학회 공지에 발표된 수학 문제를 푸는 능력을 입증하는 최초의 자동 감점 시스템이었다.

1차 정리 증명은 자동 정리 증명의 가장 성숙한 하위 분야 중 하나입니다.이 논리는 종종 합리적이고 직관적인 방법으로 임의의 문제를 특정할 수 있을 만큼 충분히 표현적이다.한편, 아직 반감정이 가능하며, 건전하고 완전한 계산이 다수 개발되어 완전 자동화 [15]시스템이 실현되고 있습니다.고차 로직과 같은 보다 표현력 있는 로직은 1차 로직보다 더 넓은 범위의 문제를 편리하게 표현할 수 있지만, 이러한 로직의 정리 증명은 [16][17]잘 개발되지 않았습니다.

벤치마크, 경쟁사 및 출처

구현된 시스템의 품질은 표준 벤치마크 사례인 수천 개의 문제(TPTP) 문제 라이브러리[18] 및 중요한 1차 문제 클래스의 많은 1차 시스템을 대상으로 매년 개최되는 1차 시스템 경연대회인 CADE ATP 시스템 경연대회(CASC)의 존재로 인해 혜택을 받았습니다.

몇 가지 중요한 시스템(모두 적어도1개의 CASC 경쟁 부문 수상)을 다음에 나타냅니다.

  • E는 완전한 1차 논리의 고성능 프로버이지만, 본래 볼프강 비벨의 지도 아래 뮌헨 공과대학의 자동 추론 그룹에서 개발되었으며, 현재는 슈투트가르트의 바덴뷔르템베르크 협력 주립대학에서 개발되었습니다.
  • 아르곤 국립 연구소에서 개발된 수달은 1차 분해능과 매개변조를 기반으로 합니다.이후 수달은 메이스4와 짝을 이루는 프로버9으로 대체되었다.
  • SETHEO는 원래 볼프강 비벨의 지휘 하에 팀이 개발한 목표 지향 모델 제거 미적분을 기반으로 한 고성능 시스템이다.E와 SETHEO는 합성정리프로버 E-SETHEO에서 (다른 시스템과) 결합되었다.
  • 뱀파이어는 원래 안드레이 보론코프와 크리스토프 호더에 의해 맨체스터 대학에서 개발되고 구현되었다.그것은 현재 성장하고 있는 국제 팀에 의해 개발되고 있다.2001년 이후 CADE ATP 시스템 대회에서 FOF 부문(다른 부문 포함)을 정기적으로 수상했다.
  • Waldmeister는 Arnim Buch와 Thomas Hillenbrand에 의해 개발된 단위 등가 1차 로직을 위한 전문 시스템입니다.그것은 14년 연속 (1997–2010) CASC UEQ 부문에서 우승하였습니다.
  • SPASS는 등식을 갖는 1차 논리 정리입니다.이것은 막스 플랑크 컴퓨터 과학 연구소의 논리 자동화 연구 그룹에 의해 개발되었습니다.

The Orem Prover Museum은 미래 분석을 위해 정리 Prover 시스템의 출처를 보존하기 위한 이니셔티브입니다. 왜냐하면 그것들은 중요한 문화적/과학적인 예술품이기 때문입니다.이것은 위에서 언급한 많은 시스템의 소스를 가지고 있습니다.

인기 있는 기술

소프트웨어 시스템

참고 항목: Proof Assistant © 비교 및 카테고리:정리 증명 소프트웨어 시스템
비교
이름. 라이선스 타입 웹 서비스 도서관 스탠드아론 최종 갱신(YYY-mm-dd 형식)
ACL2 3절 BSD 아니요. 아니요. 네. 2019년 5월
프로버9/오터 퍼블릭 도메인 TPTP 시스템 경유 네. 아니요. 2009
제이프 GPLv2 네. 네. 아니요. 2015년 5월 15일
PVS GPLv2 아니요. 네. 아니요. 2013년 1월 14일
레오 2세 BSD 라이선스 TPTP 시스템 경유 네. 네. 2013
EQP ? 아니요. 네. 아니요. 2009년 5월
슬퍼 GPLv3 네. 네. 아니요. 2008년 8월 27일
PhoX ? 아니요. 네. 아니요. 2017년 9월 28일
케이마에라 GPL Java Webstart 경유 네. 네. 2015년 3월 11일
간달프 ? 아니요. 네. 아니요. 2009
E GPL TPTP 시스템 경유 아니요. 네. 2017년 7월 4일
스나크 Mozilla Public License 1.1 아니요. 네. 아니요. 2012
뱀파이어 뱀파이어 라이선스 TPTP 시스템 경유 네. 네. 2017년 12월 14일
정리증명시스템(TPS) TPS 유통 계약 아니요. 네. 아니요. 2012년 2월 4일
SPASS FreeBSD 라이선스 네. 네. 네. 2005년 11월
이사 플래너 GPL 아니요. 네. 네. 2007
열쇠 GPL 네. 네. 네. 2017년 10월 11일
프린세스 lgpl v2.1 TPTP 상의 Java Webstart 및 시스템 경유 네. 네. 2018년 1월 27일
아이프로버 GPL TPTP 시스템 경유 아니요. 네. 2018
메타 정리 프리웨어 아니요. 아니요. 네. 2022년 7월
Z3 정리 프로버 MIT 라이선스 네. 네. 네. 2019년 11월 19일

무료 소프트웨어

독자적인 소프트웨어

「 」를 참조해 주세요.

메모들

  1. ^ Frege, Gottlob (1879). Begriffsschrift. Verlag Louis Neuert.
  2. ^ Frege, Gottlob (1884). Die Grundlagen der Arithmetik (PDF). Breslau: Wilhelm Kobner. Archived from the original (PDF) on 2007-09-26. Retrieved 2012-09-02.
  3. ^ Bertrand Russell; Alfred North Whitehead (1910–1913). Principia Mathematica (1st ed.). Cambridge University Press.
  4. ^ Bertrand Russell; Alfred North Whitehead (1927). Principia Mathematica (2nd ed.). Cambridge University Press.
  5. ^ Herbrand, Jaques (1930). Recherches sur la théorie de la démonstration.
  6. ^ Presburger, Mojżesz (1929). "Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt". Comptes Rendus du I Congrès de Mathématiciens des Pays Slaves. Warszawa: 92–101.
  7. ^ a b c d ）Davis, Martin (2001), "The Early History of Automated Deduction", in Robinson, Alan; Voronkov, Andrei (eds.), Handbook of Automated Reasoning, vol. 1, Elsevier 。
  8. ^ Bibel, Wolfgang (2007). "Early History and Perspectives of Automated Deduction" (PDF). Ki 2007. LNAI. Springer (4667): 2–18. Retrieved 2 September 2012.
  9. ^ Gilmore, Paul (1960). "A proof procedure for quantification theory: its justification and realisation". IBM Journal of Research and Development. 4: 28–35. doi:10.1147/rd.41.0028.
  10. ^ W.W. McCune (1997). "Solution of the Robbins Problem". Journal of Automated Reasoning. 19 (3): 263–276. doi:10.1023/A:1005843212881. S2CID 30847540.
  11. ^ Gina Kolata (December 10, 1996). "Computer Math Proof Shows Reasoning Power". The New York Times. Retrieved 2008-10-11.
  12. ^ David C. Luckham and Norihisa Suzuki (Mar 1976). Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records, and Pointers (Technical Report AD-A027 455). Defense Technical Information Center. Archived from the original on August 12, 2021.
  13. ^ David C. Luckham and Norihisa Suzuki (Oct 1979). "Verification of Array, Record, and Pointer Operations in Pascal". ACM Transactions on Programming Languages and Systems. 1 (2): 226–244. doi:10.1145/357073.357078.
  14. ^ D. Luckham and S. German and F. von Henke and R. Karp and P. Milne and D. Oppen and W. Polak and W. Scherlis (1979). Stanford Pascal verifier user manual (Technical Report CS-TR-79-731). Stanford University.
  15. ^ Loveland, D W (1986). "Automated theorem proving: mapping logic into AI". Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems. Knoxville, Tennessee, United States: ACM Press: 224. doi:10.1145/12808.12833. ISBN 978-0-89791-206-8. S2CID 14361631.
  16. ^ 커버, 맨프레드「1차 논리에서의 고차 정리 증명 방법」(1999년).
  17. ^ 벤츠뮐러, 크리스토프 등"LEO-II- 고전적인 고차 논리(시스템 설명)를 위한 협력 자동 정리 프로세서"자동 추론에 관한 국제 합동 회의스프링거, 베를린, 하이델베르크, 2008년
  18. ^ Sutcliffe, Geoff. "The TPTP Problem Library for Automated Theorem Proving". Retrieved 15 July 2019.
  19. ^ 번디, 앨런수학적 귀납에 의한 증명 자동화.1999.
  20. ^ 아르토시, 알베르토, 파올라 카타브리가, 귀도 거버나토리."Ked: 이원론적 정리 증명서"제11회 국제논리프로그래밍회의(ICLP'94)1994.
  21. ^ Otten, Jens; Bibel, Wolfgang (2003). "LeanCoP: Lean connection-based theorem proving". Journal of Symbolic Computation. 36 (1–2): 139–161. doi:10.1016/S0747-7171(03)00037-3.
  22. ^ Del Cerro, Luis Fariñas; Fauthoux, David; Gasquet, Olivier; Herzig, Andreas; Longin, Dominique; Massacci, Fabio (2001). "Lotrec: The Generic Tableau Prover for Modal and Description Logics". Automated Reasoning. Lecture Notes in Computer Science. Vol. 2083. pp. 453–458. doi:10.1007/3-540-45744-5_38. ISBN 978-3-540-42254-9.
  23. ^ 히키, 제이슨 등"MetaPRL – 모듈러형 논리 환경"고차 논리학의 정리 증명에 관한 국제 회의스프링거, 베를린, 하이델베르크, 2003년
  24. ^ 악어 홈페이지
  25. ^ 매스매티카 문서

레퍼런스

  • Chin-Liang Chang; Richard Char-Tung Lee (1973). Symbolic Logic and Mechanical Theorem Proving. Academic Press.
  • Loveland, Donald W. (1978). Automated Theorem Proving: A Logical Basis. Fundamental Studies in Computer Science Volume 6. North-Holland Publishing.
  • Luckham, David (1990). Programming with Specifications: An Introduction to Anna, A Language for Specifying Ada Programs. Springer-Verlag Texts and Monographs in Computer Science, 421 pp. ISBN 978-1461396871.

외부 링크