Z3：表达线性代数属性

Question

我想证明涉及矩阵和向量的表达式的属性（可能很大，但大小是固定的）。

例如我想证明一个表达式的结果是对角矩阵或三角矩阵，或者是正定的，...

为此，我想从线性代数中编码众所周知的属性和身份，例如：

||x + y|| <= ||x|| + ||y||
(A * B) * C = A * (B * C)
det(A+B) = det(A) + det(B)
Tr(zA) = z * Tr(A)
(I + AB) ^ (-1) = I - A(I + BA) ^ (-1) * B
...

我试图在 Z3 中实现这一点。但即使对于简单的属性，它也会返回未知或超时。我尝试过数组理论和量词。

我想知道这个问题是否可以用 SMT 求解器解决，还是不适合这类问题？你能举一个小例子来暗示吗？

Answer 1

您当然可以使用 Z3 来做到这一点。

我在这里构造了一个小例子，它定义了单位矩阵以及对角矩阵意味着什么，然后证明单位矩阵是对角矩阵。

所以，在Z3中做这种工作是绝对有可能的。尽管您可能会发现使用构建在 Z3 之上的工具会更好，该工具具有更多交互式验证功能，例如 Dafny 或 F*。