ブール(Boole)論理で方程式を証明する
関数FindEquationalProofは，一団の公理が方程式の形式，つまり理論の演算子から構築された式の間の等価性ですべて表されている場合，定理の証明を構築することができる．
AxiomaticTheoryを使うと，ブール論理等の理論に対する公理の集合を得ることができる．関与する演算子および定数の名前を指定することができる．束縛変数はa，b，c等の形式的な記号を使って表される．
方程式の証明を行う．
証明を，公理（緑の四角）から結果（赤い四角）に進む補題の流れを示すグラフとして表示する．三角形と円は異なるタイプの補題を表す．
または，証明のステップのすべての詳細を表示することもできる．
