뱀파이어 (테오렘 프로베라)
Vampire (theorem prover) |
| 원본 작성자 | 안드레이 보론코프[1] |
|---|---|
| 개발자 | 뱀파이어팀 |
| 안정적 해제 | 4.5.1 / 2020-07-15 |
| 리포지토리 | |
| 기록 위치 | C++ |
| 다음에서 사용 가능 | 뱀파이어 라이선스[2] |
| 유형 | 자동 정리 증명 |
| 웹사이트 | vprover.github |
뱀파이어는 맨체스터 대학의 컴퓨터 과학 학부에서 개발한 1차 고전 논리의 자동 정리 프로베른이다.버전 3까지 안드레이 보론코프가 크리슈토프 호더와 함께 개발했고, 이전까지는 알렉산드르 리아자노프와 함께 개발했다.버전 4 이후, 이 개발에는 로라 코박스, 자일스 리거, 마틴 수다 등 더 넓은 국제팀이 참여했다.1999년 이후, 가장 권위 있는 FOF 부문과 이론적 합리화 TFA 부문을 포함한 "정리 프로버를 위한 월드컵"(CADE ATP 시스템 경연대회)에서 최소 53개의 트로피를 획득했다.[3][4]
배경
뱀파이어의 낟알은 순서가 정해진 이진 분해능과 평등을 다루기 위한 중첩의 계산법을 구현한다.분할 규칙과 부등식 분할은 새로운 술어 정의의 도입과 그러한 정의의 동적 접기로 시뮬레이션할 수 있다.DPLL 방식의 알고리즘 분할도 지원된다.검색 공간의 가지치기에는 자동 삭제, 서브섬션 해결, 순서 단위 동일성에 의한 재작성, 기본성 제한 및 대체 용어의 재확보 불가능성 등 많은 표준 중복 기준과 단순화 기법이 사용된다.사용되는 감량 순서는 표준 Knuth-Bendix 순서다.
많은 효율적인 인덱싱 기법이 용어와 조항의 집합에서 모든 주요 운영을 구현하는데 사용된다.런타임 알고리즘 특수화는 전방 매칭을 가속화하는 데 사용된다.
시스템의 커널은 폐쇄적인 정상적인 형태에서만 작동하지만, 전처리기 구성요소는 완전한 1차 논리 구문의 문제를 받아들이고 이를 클로스화하며 그 결과를 커널에 전달하기 전에 많은 유용한 변환을 수행한다.정리가 증명되면 시스템은 검증 가능한 증거를 생산하게 되는데, 이것은 클로스화 단계와 결막 정상 형태의 반박을 모두 검증한다.
뱀파이어는 이론 증명과 함께 보간물을 생성하는 것과 같은 다른 관련 기능을 가지고 있다.
실행 파일은 시스템 웹 사이트에서 얻을 수 있다.[5]다소 구식인 버전은 Sigma KI의 일부로 GNU 소일반공용면허에 따라 이용할 수 있다.[6]
참조
- ^ "History". vprover.github.io. Retrieved 24 May 2018.
- ^ "Vampire Licence". vprover.github.io. Retrieved 24 May 2018.
- ^ Riazanov, A.; Voronkov, A. (2002). "The design and implementation of VAMPIRE". AI Communications. 15 (2–3/2002): 91–110. ISSN 0921-7126.
- ^ Voronkov, A. (1995). "The anatomy of vampire". Journal of Automated Reasoning. 15 (2): 237–265. doi:10.1007/BF00881918.
- ^ "Vampire". vprover.github.io. Retrieved 24 May 2018.
- ^ "CVS Info for project sigmakee". sigmakee.cvs.sourceforge.net. Retrieved 24 May 2018.
외부 링크
