6

我正在寻找 C++ 开源库（或只是开源 Unix 工具）来做：Equality test on Equations。

方程可以在运行时构建为 AST 树、字符串或其他格式。

方程大多是简单的代数方程，带有一些关于未知函数的假设。域，将是整数算术（没有浮点问题，因为相关问题是众所周知的 - 感谢@hardmath 强调它，我假设它是已知的）。

示例：输入可能包含 function phi，并带有关于它的假设（大多数情况）phi(x,y)=phi(y,x)并尝试解决：

equality_test( phi( (a+1)*(a+1) , a+b ) = phi( b+a, a*a + 2a + 1 )

它可以是模糊的或任何相等测试 - 我的意思是，它不必总是成功（即使方程相等，它也可能返回“假”）。

phi如果支持上述关于函数的假设存在问题，我可以处理这个问题，所以也欢迎简单的线性代数方程等式测试人员。

  • 你能推荐一些 C/C++ 编程库或 Unix 工具吗？（开源）
  • 如果可能的话，你能否附上一些例子，在给定的库/工具中，这样的平等测试可能是什么样子的？

PS如果这样的equal_test可以（在成功的情况下）返回同构 - （我的意思是一种“映射”） - 在两个给定的方程之间，将非常受欢迎。但是没有这种能力的工具也很受欢迎。

PS“模糊测试器”是指内部方程求解器在寻找两个函数的“同构”方面将是“模糊的”，而不是在针对随机输入的测试方面 - 我可以实现这个，当然，但我尝试找到更精确的东西。

PPS 还有另一个问题，为什么我需要更好的性能解决方案，而不是蛮力“所有输入测试”。上面的方程是我内部问题的简化形式，我没有方程中的变量之间的映射。也就是说，我有eq1=phi( (a+1)*(a+1) , a+b )和eq2=phi( l+k, k*k + 2k + 1 )，我必须找出那个a==k和b==l。但是这个子问题我可以用“蛮力”方法（甚至这种方法的渐近复杂度）来处理，如果只有几个变量，让它是 8。所以我需要为每个可能的映射做这个 equation_test。如果有一个工具可以完成整个工作，我将非常感激，并且可以为这样的项目做出贡献。但我不需要这样的功能，只需 equation_test() 就足够了，我可以轻松处理休息。

把它们加起来：

  • equal_test() 只是我必须解决的许多子问题之一，因此计算复杂性很重要。
  • 它不必是 100% 可靠的，但比仅使用一些随机输入和变量映射测试方程的可能性更高：）。
  • “是”或“否”的输出（所有附加信息可能有用，但在未来，在这个阶段我需要“是”/“否”）
4

4 回答 4

5

您的主题是自动定理证明之一，为此开发了许多免费/开源软件包。其中许多用于证明验证，但您要求的是证明搜索。

处理方程的抽象主题将是数学家称之为变体的理论。这些理论在其模型的存在性和规律性方面具有很好的性质。

您可能会想到专门处理实数或其他系统的方程，这会给寻求证明的理论添加一些公理。

如果原则上存在一种算法来确定是否可以在理论中证明逻辑陈述，则该理论称为可判定的。例如，实封闭场的理论是可判定的，正如塔斯基在 1951 年所展示的那样。然而，这种算法的实际实现缺乏并且可能是不可能的。

以下是一些可能值得学习的开源软件包，以指导您的设计和开发：

Tac：一个通用且适应性强的交互式定理证明器

Prover9：一阶和方程逻辑的自动定理证明器

E（等式）定理证明器

于 2011-08-11T13:18:05.983 回答
3

我不确定是否有任何库，但您如何通过为您的方程生成一组随机输入并将其代入必须比较的两个方程中来自己做呢。鉴于您生成大量随机数据，这将为您提供几乎正确的结果。

编辑：你也可以试试http://www.wolframalpha.com/

和

 (x+1)*(y+1) equals x+y+xy+2

和

 (x+1)*(y+1) equals x+y+xy+1
于 2011-08-11T11:10:29.910 回答
3

我认为使用反向波兰表示法可以走得很远。

  1. 用 RPN 写出你的方程

  2. 应用转换以使所有表达式具有相同的形式，例如 *A+BC --> +*AB*AC（这是 A*(B+C) --> A*B+A*C 的 RPN 等效项）， ^*BCA --> *^BA^CA (即 (B*C)^A --> B^A * C^A)

  3. “排序”对称二元运算符的参数，以便“较轻”的操作出现在一侧（例如 A*B + C --> C + A*B）

  4. 您将遇到虚拟变量的问题，例如总和指数。我认为，除了尝试在等式两边匹配它们的每一种组合之外，别无他法。

一般来说，这个问题非常复杂。

不过，您可以尝试破解：使用优化编译器（C，Fortran）并将等式的两边编译为优化的机器代码并比较输出。它可能有效，也可能无效。

于 2011-08-11T11:33:36.350 回答
1

开源 (GPL) 项目Maxima的工具类似于Wolfram Alpha 的 equals 工具：

(a+b+c)+(x+y)**2 equals (x**2+b+c+a+2*x*y+y**2)

这是is(equal())，它解决了公式：

(%i1) is(equal( (a+b+c)+(x+y)**2 , (x**2+b+c+a+2*x*y+y**2) ));
(%o1)                                true

为此，它使用有理简化器 -ratsimp，以简化两个方程的差异。当两个方程的差被简化为零时，我们知道它们对于所有可能的值都是相等的：

(%i2) ratsimp( ((a+b+c)+(x+y)**2) - ((x**2+b+c+a+2*x*y+y**2)) );
(%o2)                                  0

这个答案，只是显示方向（像其他答案一样）。如果您知道类似的东西，那可以用作 C++ Unix 程序编程库的一部分吗？与此类似的良好 C/C++ 绑定工具。请发布新答案。

于 2011-08-29T22:44:20.190 回答