编辑：现在在 SymPy 中

$ isympy
In [1]: A = MatrixSymbol('A', n, n)
In [2]: B = MatrixSymbol('B', n, n)
In [3]: context = Q.symmetric(A) & Q.positive_definite(A) & Q.orthogonal(B)
In [4]: ask(Q.symmetric(B*A*B.T) & Q.positive_definite(B*A*B.T), context)
Out[4]: True

显示其他工作的较旧答案

因此，在研究了一段时间后，这就是我发现的。

目前对我的具体问题的回答是“不，目前没有可以回答这个问题的系统。” 然而，有一些事情似乎很接近。

首先，Matt Knepley 和 Lagerbaer 都提到了 Diego Fabregat 和 Paolo Bientinesi 的作品。这项工作显示了这个问题的潜在重要性和可行性。这是一个很好的阅读。不幸的是，我不确定他的系统是如何工作的或者它有什么能力（如果有人知道关于这个主题的其他公共材料，请告诉我）。

其次，有一个为 Mathematica 编写的名为xAct的张量代数库，它可以象征性地处理对称性等问题。它在某些方面做得很好，但并不适合线性代数的特殊情况。

第三，这些规则被正式写在Coq的几个库中，这是一个自动定理证明助手（谷歌搜索 coq 线性/矩阵代数可以找到一些）。这是一个功能强大的系统，不幸的是，它似乎需要人工交互。

在与一些定理证明者交谈后，他们建议研究此类事情的逻辑编程（即 Prolog，Lagerbaer 也建议这样做）。据我所知，这还没有完成——我将来可能会玩它。

更新：我已经使用Maude system实现了这个。我的代码托管在 github

一些符号矩阵计算（例如，块矩阵完成）可以使用包 NCAlgebra http://www.math.ucsd.edu/~ncalg/（在mathematica 下运行）来完成。

Bergman http://servus.math.su.se/bergman/是 Lisp 中的一个包，具有类似的功能。

一些相关论文： http: //math.ucsd.edu/~helton/osiris/COMPALG2000/ohRevisIJC.pdf http://math.ucsd.edu/~thesis/thesis/dkronewitter/dkronewitter.pdf
http ://www. tandfonline.com/doi/abs/10.1080/00207170600882346

我认为大多数CAS系统都可以在给定符号标准正交矩阵的情况下显示这2x2一点3x3$\mathbf B$构造，例如旋转矩阵。最后，您将不得不分解结果以确定它是否是正定的。对称更容易表现出来。

那么问题就变成了，N维矩阵呢？也许您可以提出一个归纳方案，其中N-1 x N-1假设 for 为真，然后构造一个具有整体大小的新块矩阵N x N以证明它是正定且对称的。

所以最后一个问题，哪个软件更适合该任务（如果有的话），我的经验一直是MATLAB/MuPad并且Derive（仍然使用它）并且它们都不能很好地处理向量和矩阵。MATLAB将所有内容分解为组件，并且Derive可以声明Non-scalars但不对它们应用任何简化规则。

我希望这篇文章能够对这种“漏洞”以及如何填补它提供更多的见解。对我来说，我想要一些软件来帮助我简化向量的多个点积和叉积的表达式，以及使用众所周知的恒等式的旋转矩阵，例如：$\vec a \times (\vec b \times \vec c) = (\vec a \cdot \vec b)\vec c - (\vec a \cdot \vec c) \vec b$

Maple 15 做不到。它没有矩阵的“正交”属性（尽管它有 Symmetric 和 PositiveDefinite）。