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求解器来解决这个问题，还是说它不适合这种类型的问题？你能否通过给出一个小例子来提示一下？

- tyr.bentsen

---

你肯定可以对这些属性进行编码；并且可能会在“足够小”的尺寸上证明它们。你的领域也很重要：整数，实数？后者有一个可判定的理论，而前者可能会导致求解器报告“未知”，因为你将处理非线性丢番图方程。对于“所有尺寸”的证明需要量词，并且除非它们像求解器不做归纳那样微不足道，否则不太可能被证明。在任何情况下，如果不尝试，就无法知道。请分享您的学习心得！ - alias

Answer 1

您可以使用Z3来完成这个任务。

我已经构建了一个小例子，在这里定义了单位矩阵和对角矩阵的含义，并证明了单位矩阵是对角矩阵。

因此，使用Z3进行这种工作是完全可能的。但是您可能会发现，使用基于Z3构建的工具（如Dafny或F*）具有更多交互式证明功能，会更加方便。

- James Wilcox