我正在寻找一个工具（最好是GUI，但CLI也可以），允许我输入数学表达式并对其进行操作，但限制我只能使用数学上有效的操作。此外，该工具必须能够保存会话，并在以后证明给定的一组保存的操作是有效的。 注意：我不是在寻找一个系统来生成证明，只是检查我手动指定的步骤是否有效。 我已经使用ACL2执...