問題タブ [first-order-logic]

私はドキュメントとガイドをよく見て、かなりのことを自分で試しました。しかし、私の問題の解決策は私を回避します。

これはチュートリアルがレコードに関して述べていることですが、それを私のニーズに合わせる方法は私には不明です:

5 つのフィールド、2 つの Int、3 つの Bool のレコードを宣言するための SMT-LIB2 構文を探しています。

次に、これらのレコードの配列/セットが必要です。

さらに、レコードのセットに対して $\forall$ ステートメントを作成するために使用する構文を探しています。

与えられたリソースで最善を尽くしましたが、どこにも行きませんでした。

ありがとう。

自動定理証明器 SPASS を使用して、一次論理でいくつかのハードウェアをモデル化しようとしています。

したがって、論理文で使用できるようにするには、真/偽の値 (事前定義されたもの) を取ることができる信号が必要です。

SPASS は、ユーザーが自分で定義できるある種のタイプ (ソートと呼ばれる) をサポートしています。

true/false の事前定義されたタイプがあるかどうか疑問に思っていますか?

型がなくてもこれを回避できると思います.. True(SIGNAL) と False(SIGNAL) の形式の述語を使用し、SIGNAL = T の場合は True(SIGNAL) が true を返し、SIGNAL = F の場合は false (T とF は定数です) が、定義済みの true/false を使用した方がよかったと思います。

Z3 を使用してレコードの配列を作成することができましたが、配列に対して $\forall$ 操作を実行するために必要な構文を確認するのに苦労しています... これまでに持っている SMT-LIB2 コードのスニペット サンプルです。 .

最後から 3 番目の行には配列への参照が必要だと思いますが、すべてを試しましたが、チュートリアルはこの問題の解決に役立ちませんでした。

ここにある配列に対して $\forall$ 操作を実行するにはどうすればよいですか?