증명과 반례의 다른 방향
가정에서 목표가 따라오는지 증명하는 작업과 목표를 깨는 모델을 찾는 작업은 접근이 다르다. Prover9와 Mace4는 이런 두 방향의 분석에 활용할 수 있다. 한쪽이 제한 시간 내 결과를 내지 못했다고 다른 쪽 결과가 자동으로 정해지는 것은 아니다.
논리 문제로 모델링
일차 논리와 등식으로 가정과 확인할 성질을 표현한다. 탐색은 작성한 형식 문제를 대상으로 진행되므로 변수 범위와 전제의 의미를 검토해야 한다. 도구가 찾아낸 증명이나 모델을 원래 질문에 연결하는 해석도 필요하다.
기존 배포와 새 계열
원래 프로젝트 안내는 개선된 LADR-2026 계열의 새 배포 위치를 가리킨다. 이 계열은 기존 입력 호환성과 TPTP 입력 및 TSTP 출력 지원을 안내한다. 과거 실험을 재현한다면 실행한 배포판과 옵션을 명확히 구분한다.