문제와 해법을 공유하기
TPTP 문제 라이브러리는 자동 증명 시스템을 시험할 문제들을 모은다. TSTP는 이러한 문제의 해법을 다루는 별도 자료 모음이다. 문제의 논리적 조건과 결과의 표현을 맞추면 도구 사이의 비교와 재사용이 쉬워진다.
언어와 판정의 구분
TPTP 언어는 문제와 해법을 작성하는 데 쓰이며 SZS는 논리적 상태와 결과를 표현하는 값들을 제공한다. 파일을 문법에 맞게 작성했다는 사실과 원하는 논리 문제를 정확히 표현했다는 사실은 다르다. 증명기의 지원 구문도 확인한다.
실험을 위한 기반
온라인 도구는 문제 준비, 증명기 실행, 해법 확인 같은 작업을 지원한다. 연구 결과를 비교할 때는 같은 문제 집합뿐 아니라 제한 시간과 자원, 판정 기준을 맞춰야 한다. 문제 라이브러리 자체가 모든 시스템의 품질을 대신 평가하지는 않는다.