Z3：表达线性代数性质答案

【问题标题】：Z3: express linear algebra propertiesZ3：表达线性代数性质
【发布时间】：2018-04-20 07:15:29
【问题描述】：

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

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

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

||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 求解器来解决，或者它是否不适合这类问题？可以举个小例子给个提示吗？

【问题讨论】：

你当然可以对这些属性进行编码；并可能证明它们“足够小”的尺寸。您的域也很重要：整数，实数？后者有一个可判定的理论，而前者可能导致求解器报告unknown，因为您将处理非线性丢番图方程。 “所有规模”的证明都需要量词，除非它们是微不足道的，因为求解器不进行归纳，否则不太可能得到证明。无论哪种情况，不尝试都不可能知道。请分享你的经验！

【解决方案1】：

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

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

所以，在 Z3 中做这样的工作肯定是可以的。尽管您可能会发现使用基于 Z3 构建的具有更多交互式验证功能（例如 Dafny 或 F*）的工具会更好。

【讨论】：