Z3：線形代数を表現する

Question

行列やベクトルを含む式の性質を証明したいと考えています（サイズは大きくなる可能性がありますが、サイズは固定されています）。

Iは、式の結果は、対角行列または三角行列である、またはそれは、正定であることを証明したい例えば

...

そのために私は、エンコードよく知られた特性をたいと思いますし、以下のような線形代数からアイデンティティ、：

||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を使用できます。

私は、恒等行列とそれが対角行列であることを定義する小さな例hereを構築し、次に恒等行列が対角であることを証明しました。

したがって、Z3でこの種の作業を行うことは間違いありません。 DafnyやF *など、よりインタラクティブな検証機能を備えたZ3の上に構築されたツールを使用すると、より良い時間を得ることができます。