진리나무 (Semantic Tableau)

전제와 결론을 넣으면 진리나무를 자동으로 전개하여 타당성을 판정합니다. 문장논리·술어논리 모두 지원합니다.

술어논리 진리나무는 일반적으로 결정불가능(undecidable)합니다. 이 도구는 최대 전개 횟수를 두어, 한도 내에 끝나지 않으면 "확실치 않음"으로 표시합니다.