数式を入力して操作を実行できるが、数学的に有効な操作のみに制限するツール (GUI が推奨されますが、CLI が機能します) を探しています。また、ツールはセッションを保存し、保存された特定の一連の操作が有効であることを後で証明できる必要があります。
注:証明を生成するシステムを探しているのではなく、手動で指定した手順が有効であることを確認するだけです。
同様の操作にACL2を使用したことがありますが、一部のケースではうまく機能しますが、それ以外の場合は非常に使いにくいです。
この小さなプロジェクトが私のモチベーションです。方程式を解くことができる D テンプレート タイプです。この方程式を考えると：
(A * B) = C + D / F;
シンボルのいずれかを不明として設定でき、その式を評価すると、その変数に割り当てられます。これは、式ツリーを型に組み込み、書き換え規則を使用してそれを未知の型に対応できるものに変換することによって機能します。
必要なのは、書き換えルールを検証する方法です。それらは、ある関係が真であり、別の関係も真であるというアサーションをテストすることによって検証できます。