1

これは、Z3 の Model-based Quantifier Instantiation (MBQI) と階層化された並べ替えフラグメントに関する以前の質問のフォローアップです(素早い回答をくれた Leonardo de Moura に再び感謝します)。

多ソート ロジックの決定可能なフラグメントに関する論文 [Abadi et al., Decidable fragment of many-sorted logic, LPAR 2007] で、著者は有限モデル プロパティで決定可能な多ソート ロジックのフラグメント St1 について説明しています。

このフラグメントでは、Z3 ドキュメントで説明されているように、並べ替えを階層化する必要があり、式 F が (スコーレム化された) プレネックス正規形である必要がありますが、追加の原子式を使用できます。

y in Im[f]

の「短縮形」である F で発生する

存在 x1 : A1, ..., xn : An . y = f(x1,...,xn)

ここで、f はシグネチャ f : A1 x ... x An -> B を持つ関数であり、f は範囲 B を持つ唯一の関数でなければなりません。したがって、St1 フラグメントは (非常に制限された方法で) 成層化に違反することを許可します。たとえば、f が全射であることを主張するためです。

これが未解決の研究課題であるかどうかはわかりません。Z3 の MBQI 決定手順が St1 フラグメントで完了しているかどうかを誰か知っていますか? Z3 は有限時間後に F に対して (理論的には) SAT または UNSAT を生成しますか?

4

1 に答える 1

2

最初に、1 つの明確化、原則として、MBQI は重層化されたマルチソートされたフラグメントを決定できます。その正当性は、 http://research.microsoft.com/en-us/um/people/leonardo/ci.pdf (*)のセクション 4.1 に記載されています。ただし、Z3 4.0 は、セクション 4.1 で提案されている追加ルールの実装をサポートしていません。そのため、Z3 4.0unknownは、このフラグメントに含まれる数式で失敗する (返される) 場合があります。アルゴリズムと現在の Z3 を使用した実際の実装との区別を明確にしたいだけです。

あなたの質問に関しては、はい MBQI フレームワークは、展開された述語を含む階層化された式を決定できますy in Im[f]。この述語は肯定的にしか発生しないと思います。つまり、not y in Im[f]これに相当するものはありません

forall x1:A1, ...,xn:An. y != f(x1, ... xn)

が正にのみ発生する場合y in Im[f]、それを展開することができ、スコーレム化の後、フォームの基底公式が得られy = f(k1, ..., kn)ます。F*(*) で定義されたセットはまだ有限であるため、MBQI は依然として決定手順です。F*層化が普遍的な式の中で壊れている場合にのみ、無限になる可能性があります。

于 2012-05-31T18:36:34.933 に答える