古典論理では含意が否定と論理和で表されます．このことは良く知られています． 本自動証明器もこのことを暗黙で使っています． 他にも論理和や論理積の分解規則など，オリジナルのLKの推論規則にはない規則も使います． これらの派生推論規則がLKで妥当であることは演習問題でした． また証明図は公理まで展開せずに，シーケントの両辺が同じ論理式を含むところまでで展開をストップしています．それが妥当であることもLKのWeakening(増)規則から明らかでしょう． また同値記号などは`マクロ記号'として扱っています．それらの記号は証明図には表れません．
使い方： 上の入力欄に命題論理式を入力し，そのとなりにあるボタンを押します， あるいは，選択欄から論理式を選択し，入力に欄にコピーして（マウスボタンを離すと自動コピー）からボタンを押します．
入力に使える論理結合子は次のとおりです:
| * | AND | $\wedge$ |
| + | OR | $\vee$ |
| > | 含意 | $\rightarrow$ |
| ! | 否定 | $\neg$ |
| < | 逆向きの含意 | $\leftarrow$ |
| <> | 同値 | $\equiv$ |
たとえば， $\neg A \wedge B \rightarrow C$ は ! A * B > C と書きます． このように，通常の論理記号と違います．Prologの構文に合わせることにより入力論理式のパージングという大変な部分の作成を省くためです．
入力論理式の長さには制限があります．論理記号が全部で15個程度までです．（今ははずしています．）
このCGIはSWI-Prologで書かれています．