자동 추론의 질문
명시한 가정과 추측을 입력하면 논리적 관계를 분석한다. 증명 탐색뿐 아니라 유한 모델을 구성하는 기능도 있다. 증명과 반례는 서로 다른 형태의 산출물이므로 어떤 질문에 대한 결과인지 구분해 읽어야 한다.
여러 전략을 적용하기
포트폴리오 모드는 여러 추론 전략을 시도한다. 만족 가능한 문제에 맞는 전략 묶음도 따로 제공한다. 단일 전략과 포트폴리오의 성능은 문제와 시간 제한에 따라 달라지므로 같은 조건에서 비교해야 한다.
지원 범위 확인
산술과 배열, 자료형의 조합 등 일차 논리 이외의 기능도 발전하고 있다. 그렇다고 모든 SMT 문제나 고차 논리를 같은 수준으로 지원한다고 가정하면 안 된다. 입력 논리와 옵션, 출력된 증명 및 모델 정보를 함께 검토한다.
관련 문서
E 자동 정리 증명기 / TPTP / Isabelle / Z3