패러독스 (테오렘 프로베라)

Paradox (theorem prover)
역설
개발자
  • 쿤 린드스트룀 클라센
  • 니클라스 쇠렌손
유형자동화된 정리 증명

패러독스는 샬머스 공과대학의 쿤 린드스트룀 클라센과 니클라스 소렌손이 개발한 평등성을 지닌 순수 1차 논리(FOL)를 위한 유한 도메인 모델파인더다.[1][2]자동화된 정리 증명 시스템의 일부로서 참여할 수 있다.[citation needed]이 소프트웨어는 주로 하스켈 프로그래밍 언어로 작성된다.[3]GNU General Public License의 조건에 따라 발매되며 무료다.[4]

특징들

패러독스 개발자들은 이 소프트웨어를 매큐네라는 이름의 도구를 따온 메이스식 방법이라고 설명했다.[5][6]패러독스는 버전 4까지 개발되었으며, 최종 버전은 Web Ontology Language OWL2 모델 발굴에 효과적이다.[7]

경쟁

패러독스는 2003년부터 2012년까지 매년 자동화된 정리 증명 대회인 CAAD ATP 시스템 경연대회에서 부문별 우승자였다.[8]

참조

  1. ^ "Paradox". Chalmers University of Technology. Archived from the original on 8 January 2007. Retrieved 26 May 2007.
  2. ^ Pudlák, Petr (17 July 2007). "Semantic Selection of Premisses for Automated Theorem Proving" (PDF). In Urban, J.; Sutcliffe, G.; Schulz, S. (eds.). Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. The 21st International Conference on Automated Deduction. CEUR Workshop Proceedings. Vol. 257. Bremen. pp. 27–44. ISSN 1613-0073. Archived from the original (PDF) on 7 November 2018. Retrieved 7 November 2011.
  3. ^ "Entrants' System Descriptions". University of Miami. Paradox 3.0. Archived from the original on 7 November 2018. Retrieved 7 November 2018.
  4. ^ "Paradox". Chalmers University of Technology. Archived from the original on 15 January 2007. Retrieved 30 April 2020.
  5. ^ Claessen, Koen; Sörensson, Niklas. "New Techniques that Improve MACE-style Finite Model Finding" (PDF). Archived from the original (PDF) on 11 November 2018. Retrieved 11 November 2018.
  6. ^ "Automated Theorem Proving" (PDF). Australian National University College of Engineering & Computer Science. pp. 73–74. Archived (PDF) from the original on 11 November 2018. Retrieved 11 November 2018.
  7. ^ Schneider, Michael; Sutcliffe, Geoff (2011). "Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving". arXiv:1108.0155 [cs.AI].
  8. ^ "The CADE ATP System Competition - The World Championship for Automated Theorem Proving". Previous CASCs' Division Winners. Archived from the original on 1 September 2018. Retrieved 7 November 2018.


Stub icon

이 컴퓨터 과학 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.

Stub icon

이 무료 오픈소스 소프트웨어 기사는 단조롭다.위키피디아를 확장하여 도울 수 있다.