Your topic is one of automated theorem proving, for which a number of free/open source software packages have been developed. Many of these are meant for proof verification, but what you ask for is proof searching.
Dealing with the abstract topic of equations would be the theories mathematicians call varieties. These theories have nice properties with respect to the existence and regularity of their models.
It is possible you have in mind equations that deal specifically with real numbers or other system, which would add some axioms to the theory in which a proof is sought.
If in principle an algorithm exists to determine whether or not a logical statement can be proven in a theory, that theory is called decidable. For example, the theory of real closed fields is decidable, as Tarski showed in 1951. However a practical implementation of such an algorithm is lacking and perhaps impossible.
Here are a few open source packages that might be worth learning something about to guide your design and development:
I am not sure for any library but how about you do it yourself by generating a random set of inputs for your equation and substituting it in both equations which have to be compared. This would give you a almost correct result given you generate considerable amount of random data.
I think you can get pretty far with using Reverse Polish Notation.
Write out your equation using RPN
Apply transformations to bring all expressions to the same form, e.g. *A+BC --> +*AB*AC (which is the RPN equivalent of A*(B+C) --> A*B+A*C), ^*BCA --> *^BA^CA (i.e. (B*C)^A --> B^A * C^A)
"Sort" the arguments of symmetric binary operator so that "lighter" operations appear on one side (e.g. A*B + C --> C + A*B)
You will have problem with dummy variables, for example sum indices. There is no other way, I think, but to try every combination of matching them on both sides of the equation.
In general, the problem is very complicated.
You can try a hack, though: use an optimizing compiler (C,Fortran) and compile both sides of the equation to optimized machine code and compare the outputs. It may work, or may not.
For this purpose, it uses rational simplifier - ratsimp, in order to simplify the difference of two equations. When difference of two equations is simplified to zero, we know they are equal for all possible values:
This answer, just shows direction (like other answers). If you know about something similar, that can be used as a part of C++ Unix program - programming library ? Good C/C++ binding similar tool to this. Please, post new answer.
发布评论
评论（4）
您的主题是自动定理证明之一，许多免费/开源软件包都提供了该主题已开发。其中许多是为了证明验证，但您要求的是证明搜索。
处理方程这一抽象主题的理论被数学家称为变量。这些理论在其模型的存在性和规律性方面具有良好的特性。
您可能想到的是专门处理实数或其他系统的方程，这将为寻求证明的理论添加一些公理。
如果原则上存在一种算法来确定某个逻辑陈述是否可以在理论中得到证明，则该理论称为“可判定的”。例如，实闭域理论是可判定的，正如 Tarski 在 1951 年所展示的那样。这种算法的实现是缺乏的，也许是不可能的。
以下是一些可能值得学习的开源软件包，可以指导您的设计和开发：
Tac：A通用且适应性强的交互式定理证明器
Prover9：自动定理证明器一阶和方程逻辑
E(quational) 定理证明者
Your topic is one of automated theorem proving, for which a number of free/open source software packages have been developed. Many of these are meant for proof verification, but what you ask for is proof searching.
Dealing with the abstract topic of equations would be the theories mathematicians call varieties. These theories have nice properties with respect to the existence and regularity of their models.
It is possible you have in mind equations that deal specifically with real numbers or other system, which would add some axioms to the theory in which a proof is sought.
If in principle an algorithm exists to determine whether or not a logical statement can be proven in a theory, that theory is called decidable. For example, the theory of real closed fields is decidable, as Tarski showed in 1951. However a practical implementation of such an algorithm is lacking and perhaps impossible.
Here are a few open source packages that might be worth learning something about to guide your design and development:
Tac: A generic and adaptable interactive theorem prover
Prover9: An automated theorem prover for first-order and equational logic
E(quational) Theorem Prover
我不确定是否有任何库，但是您自己如何通过为方程生成一组随机输入并将其替换到必须比较的两个方程中来实现。如果您生成大量随机数据，这将为您提供几乎正确的结果。
编辑：
和
您也可以尝试使用 http://www.wolframalpha.com/
I am not sure for any library but how about you do it yourself by generating a random set of inputs for your equation and substituting it in both equations which have to be compared. This would give you a almost correct result given you generate considerable amount of random data.
Edit:
Also you can try http://www.wolframalpha.com/
with
and
我认为使用逆波兰表示法可以取得很大的成果。
使用 RPN 写出您的方程
应用变换使所有表达式变为相同的形式，例如 *A+BC --> +*AB*AC（相当于 A*(B+C) --> A*B+A*C 的 RPN），^*BCA --> *^BA^CA（即（B*C）^A --> B^A * C^A）
对对称二元运算符的参数进行“排序”，以便“较轻”的操作出现在一侧（例如A*B + C --> C + A*B)
对
你会虚拟变量存在问题，例如总索引。我认为，没有其他方法，只能尝试在等式两边匹配它们的每种组合。
一般来说，问题是非常复杂的。
不过，您可以尝试一下 hack：使用优化编译器（C、Fortran）并将方程两边编译为优化的机器代码并比较输出。它可能有效，也可能无效。
I think you can get pretty far with using Reverse Polish Notation.
Write out your equation using RPN
Apply transformations to bring all expressions to the same form, e.g. *A+BC --> +*AB*AC (which is the RPN equivalent of A*(B+C) --> A*B+A*C), ^*BCA --> *^BA^CA (i.e. (B*C)^A --> B^A * C^A)
"Sort" the arguments of symmetric binary operator so that "lighter" operations appear on one side (e.g. A*B + C --> C + A*B)
You will have problem with dummy variables, for example sum indices. There is no other way, I think, but to try every combination of matching them on both sides of the equation.
In general, the problem is very complicated.
You can try a hack, though: use an optimizing compiler (C,Fortran) and compile both sides of the equation to optimized machine code and compare the outputs. It may work, or may not.
开源 (GPL) 项目 Maxima 具有类似于 Wolfram Alpha 的equals工具：
这是is(equal())，解决公式：
为此目的，它使用 有理简化器 -ratsimp，以简化两个方程的差异。当两个方程的差简化为零时，我们知道它们对于所有可能的值都相等：
这个答案仅显示方向（与其他答案一样）。如果您知道类似的东西，可以用作 C++ Unix 程序的一部分 - 编程库 ？ 与此类似的良好 C/C++ 绑定工具。 请发布新答案。
Opensource (GPL) project Maxima has tool simmilar to Wolfram Alpha's equals tool :
Which is is(equal()), that solves formulas :
For this purpose, it uses rational simplifier - ratsimp, in order to simplify the difference of two equations. When difference of two equations is simplified to zero, we know they are equal for all possible values:
This answer, just shows direction (like other answers). If you know about something similar, that can be used as a part of C++ Unix program - programming library ? Good C/C++ binding similar tool to this. Please, post new answer.