Z3: express linear algebra properties

Question

I would like to prove properties of expressions involving matrices and vectors (potentially large size, but size is fixed).

For example I want to prove that the outcome of an expression is a diagonal matrix or a triangular matrix, or it is positive definite, ...

To that end I'd like encode well known properties and identities from linear algebra, such as:

||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
...

I have attempted to implement this in Z3. But even for simple properties it returns unknown or times out. I've tried with array theory and quantifiers.

I'd like know if this problem can be solved with an SMT solver or is it not suited for these kind of problems? Could you give a hint by giving a small example?

Gearhart

You can surely encode such properties; and possibly prove them for "small enough" sizes. Your domain would be important as well: Over integers, reals? Latter has a decidable theory, while the former can lead to solver reporting unknown since you'll be dealing with non-linear Diophantine equations. Proofs for "all sizes" would require quantifiers, and are unlikely to be proven unless they are trivial as solvers don't do induction. In either case, it's impossible to know without trying. Please share your learnings! – Conglomerate

Answer 1

You can certainly use Z3 to do this.

I have constructed a small example here, which defines the identity matrix and what it means to be a diagonal matrix, and then proves that the identity matrix is diagonal.

So, it is definitely possible to do this kind of work in Z3. Though you may find you have a better time using a tool built on top of Z3 that has more interactive proving features, such as Dafny or F*.

Octuple