方程式等式测试(在C++中或使用Unix工具)(代数函数同构)

Question

我正在寻找C++开源库(或者只是开源的Unix工具):方程式上的等式测试.

方程式可以在运行时期间构建为AST树,字符串或其他格式.

方程式主要是简单的代数方程式,对未知函数有一些假设.域,将是整数算术(没有浮点问题,因为相关问题是众所周知的 - 感谢@hardmath强调它,我认为它是已知的).

示例:输入可能包含函数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如果这样的equality_test可以(在成功的情况下)返回同构 - (我的意思是,一种"映射") - 在两个给定的方程之间,将非常受欢迎.但是,没有这种功能的工具也非常受欢迎.

PS通过"模糊测试器"我的意思是内部方程求解器在寻找两个函数的"同构"方面将是"模糊的",而不是在对随机输入的测试方面 - 我可以实现这一点,当然,但我尝试找到更精确的东西.

PPS还有另一个问题,为什么我需要更好的性能解决方案,而不是暴力"所有输入测试".上面的公式是我的内部问题的simplyfied形式,在这里我没有在方程的变量之间的映射.也就是说,我有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()即可,我可以轻松处理休息.

把它们加起来:

• equality_test()只是我必须解决的许多子问题之一,因此计算复杂性很重要.
• 它不一定是100%可靠,但更高的可能性,而不仅仅是测试具有一些随机输入和变量映射的方程式非常受欢迎:).
• 输出"是"或"否"(所有其他信息可能有用,但将来,在此阶段我需要"是"/"否")

Answer 1

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

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

你可能会想到专门处理实数或其他系统的方程式,这会为寻求证据的理论增加一些公理.

如果原则上存在一种算法来确定逻辑陈述是否可以在理论中得到证实,那么该理论就被称为可判定的.例如,真实封闭场的理论是可判定的,正如塔斯基在1951年所展示的那样.然而,这种算法的实际实现是缺乏的,也许是不可能的.

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

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

Prover9:一阶和等式逻辑的自动定理证明器

E(quational)定理证明