z3.Realの行列をZ3に宣言できることは、その要素を個別に宣言することによって（おそらくリスト内包によって）知ることができます。未知のサイズの行列を表現する方法はありますか？Z3で未知のサイズの行列を宣言する
は、例えば、次の例を考える：画像フィルタで を、画像IとKがI*Kあるフィルタカーネルとの間の畳み込み、size [X,Y]の画像Iとフィルタカーネルsize [M,N]のK所与。私はZ3がI*K == I*F1*F2のような任意のサイズのフィルタF1とF2が存在することを証明（または反証）したいと思います。
問題自体は完全に構成されており、おそらく意味がありません。考え方は、Z3に、行列が線形関数で表現できる一定の性質を満たすように未知のサイズの行列を求めるように依頼できるかどうかです。ありがとう！
Z3は、単純型の1次論理仕様をサポートしています。ある意味で、最初の疑問は、あなたが論理に関心を持つあなたの特性をどう表現するかということです。 制限付きサイズのモデルでは、サイズX、Y、M、Nをインスタンス化して、適切な有限ドメインに対する反例クエリを表現できます。パラメトリックサイズが必要な場合は、*の動作を三項関係として表現します。たとえば、2つの引数を取り、I、Kの項目にI_K（x、y）がどのように関係するかを表現する関数I、K、I_Kを使用できます。 Lean、PVS、Coq、Isabelle、Dafnyなどの環境など、相互作用を良好にサポートしている環境は、校正の設定に適しています。
ニコライの答えは頭の爪に当たっているようです。 Z3（または任意のSMTソルバー）は、「不明な」サイズの行列について考えるときに、そのような問題に取り組むための最良のツールではないと思います。問題の具体例があるときは、Z3は非常に効果的だと思います。しかし一般的な "フォーラルサイズ"の場合はそうではない。これらの主張は、通常、帰納的な証明が必要で、他のツールに適しています。
ただし、解釈されない関数を使用しないでください。行列とフィルタを未解釈の関数として表現し、畳み込みをその点でコード化するならば。 NxMの上限（つまりN < 100、M < 100など）を想定し、境界外のものが適切な結果を生むようにコードを作成する必要があります。 （もちろんそれは手元の問題に左右されます）
私はそれがあなたにかなり良い結果を与えるだろうと思うので、涼しいZ3がその設定の下にいかれるか驚くかもしれません。私はあなたがこのアプローチを試してみると、あなたが知っていることを聞くのが大好きです。