프로베라9

Prover9

프로베라9는 윌리엄 맥쿠네가 개발한 1차 및 등가 논리의 자동화된 정리 프로베라다.

설명

프로베라9는 윌리엄 맥쿤이 개발한 오터 정리 프로베러의 후속작이다.[1]: 1 프로베라9는 비교적 읽을 수 있는 증거를 생산하고 강력한 힌트 전략을 가지고 있는 것으로 유명하다.[1]: 11

프로베라9는 유한 모델과 백작샘플을 검색하는 메이스4와 의도적으로 짝을 이룬다.둘 다 동일한 입력에서 동시에 실행될 수 있으며,[2] Prober9는 증거를 찾으려고 시도하고, Mace4는 (검증) 대례를 찾으려고 시도한다.Prober9, Mace4 및 기타 많은 도구는 LADR("자동화 공제 연구를 위한 도서관")이라는 이름의 기반 라이브러리에 구축되어 구현을 단순화한다.결과물은 ACL2를 이용해 별도로 검증한 증명확인 도구 아이비(Ivy)가 더블 체크할 수 있다.

2006년 7월에 LADR/Prover9/Mace4 입력 언어는 주요한 변화를 일으켰다(또한 Otter와 구별된다)."clauss"와 "formula"의 핵심 구분이 완전히 사라졌고, "formula"는 이제 자유 변수를 가질 수 있으며, "clauss"는 "formula"의 하위 집합이 되었다.Prober9/Mace4는 또한 "골" 형태의 공식을 지원하는데, 이것은 자동적으로 증거를 위해 부정된다.Prober9는 기본적으로 자동으로 증거를 생성하려고 시도하지만, 반대로 Otter의 자동 모드를 명시적으로 설정해야 한다.

프로베라9는 2009년까지 매달 또는 격월로 신제품을 출시하는 등 활발한 개발 중에 있었다.Prober9는 무료 소프트웨어로서 오픈 소스 소프트웨어로서 GPL 버전 2 이상에서 출시된다.

예

소크라테스

전통적인 "모든 인간은 죽는다"인 "소크라테스는 사람이다"는 "소크라테스는 죽는다"는 것이 프로베라9에서 이렇게 표현될 수 있다.

공식(공식). man(x) -> male(x). 자유 변수 x man(공식)이 있는 % 공개 공식.end_of_list. 
수식(수식)필멸의end_of_list.

이것은 자동으로 폐쇄 형태로 변환될 것이다(Probr9도 이를 받아들인다). 

수식(수식)-man(x) man(x) man(man) man(mal) man(-csi(csi).end_of_list.

2의 제곱근은 불합리하다.

2의 제곱근이 비이성적이라는 증거는 다음과 같이 표현할 수 있다.[3]

수식(수식)1*x = x.                            % identity   x*y = y*x.                          % commutativity   x*(y*z) = (x*y)*z.                  % associativity   ( x*y = x*z ) -> y = z.             % cancellation (0 is not allowed, so x!=0).   %   % Now let's define divides(x,y): x divides y.   %   Example: divides(2,6) is true because 2*3=6.   %   d만약 2x*x을 나누Ivides(x, y)<>->,(zx*z)y이 존재하). divides(2,x*x)->, divides(2,x).%,.;divides(x,b)).%a/b 최저 조건 2에 있어요!=1.인데 a*a)2*(b*b)%a/b)sqrt(2), 그렇게 a^2=2*b^2.(x!=1)-> -(분열(x,a)및%오리지널 작가 알을 나눕니다.가장 이 않은 아버님을요. end_of_list.

참조

  1. ^ a b Phillips, J. D.; Stanovsky, David. "Automated Theorem Proving in Loop Theory" (PDF). Charles University. Archived (PDF) from the original on 28 March 2018. Retrieved 15 November 2018.
  2. ^ Berghammer, Rudolf; Struth, Georg (21 June 2010). "On Automated Program Construction and Verification" (PDF). In Bolduc, Claude; Desharnais, Jules; Ktari, Bechir (eds.). Mathematics of Program Construction, Proceedings. 10th International Conference, MPC 2010. Quebec City. doi:10.1007/978-3-642-13321-3. ISBN 978-3-642-13320-6. Archived from the original (PDF) on 19 November 2018. Retrieved 19 November 2018.
  3. ^ Wheeler, David A. "sqrt2.in". David A. Wheeler’s Personal Home Page. Retrieved 14 March 2016.

외부 링크