명제논리식의 진리함수를 계산하고 이것을 나타내는 진리표를 그리는 웹프로그램. [예]

논리도해는 명제논리식들이 만족불가능임을 기계적으로 증명한다. 모델집합이 공집합에 가까울 때는 이 집합을 용이하게 계산할 수 있다. [예]

명제논리 피치 증명시스템의 형식증명을 작성하고 각 라인의 타당성을 입증한다. 1계논리 피치 증명시스템의 입문과정이다. [예]

1계논리 피치 증명시스템은 엄격한 수학을 증명하는 인간의 사고과정을 그대로 반영한다. [예]