量詞實例化和許多排序邏輯

Question

的St1的片段這是一個後續我previous question在Z3的基於模型的 量詞實例化（MBQI）和分層的各種片段（感謝 再次萊昂納多·德莫拉爲了快速回答）。

在其上的許多排序邏輯的可判定片段紙[阿巴迪等 人，許多排序邏輯的可判定的片段，LPAR 2007]中，作者 描述的片段許多排序邏輯的St1中即可判定與一個 有限模型屬性。

該片段需要的種類是分層和公式F是在作爲Z3 文檔中描述（skolemized）前束範式，但允許額外的原子公式以lm並[f

ÿ ]

F中，這是一個 「的簡寫」 爲

發生存在X1：A1，...，XN：一個。 y = f（x1，...，xn）

其中f是帶簽名f：A1 x ... x An - > B的函數，f必須是範圍爲B的唯一函數。因此，St1片段允許（以非常有限的方式）違反分層，例如爲了斷定f是完全的。

我不確定這是否可能是一個開放的研究問題： 有人知道Z3的MBQI決策程序是否爲St1片段的完整 ？在有限的時間之後，Z3是否會產生（理論上）SAT或 UNSAT for F？

Answer 1

首先，一個澄清，原則上，MBQI可以決定分層多重排序片段。理由在http://research.microsoft.com/en-us/um/people/leonardo/ci.pdf（*）的第4.1節中給出。但是，Z3 4.0不支持實施4.1節中建議的附加規則。因此，Z3 4.0可能會失敗（返回unknown）在此片段中的公式。我只想說明算法與使用當前Z3的實際實現之間的區別。

關於你的問題，是的MBQI框架可以決定包含擴展謂詞y in Im[f]的分層公式。我假設這個謂詞只出現在正面。 也就是說，我們沒有not y in Im[f]這相當於

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

如果發生y in Im[f]只有積極，那麼它可以擴展，並skolemization後，我們有如下形式y = f(k1, ..., kn)的地面公式。 MBQI仍然是一個決策程序，因爲（*）中定義的集合F*仍然是有限的。 F*只有當分層在通用公式內部被破壞時纔可能變得無限。