對於空模型處理量化公式的正確方法是什麼？

Question

我在玩未解釋的排序和函數，並不能完全理解量化公式如何與空模型進行交互。這裏（這裏也http://rise4fun.com/Z3Py/6ets）是有點迷惑了我一些簡單的例子：

1. [∀v : False]是不飽和度，而「直覺」它擁有一個空模型。
2. 檢查[∃v : v = v]產生一個空模型，但沒有令人滿意的分配。
3. 某些公式，看似等價於[∃v : v = v]，以某種方式阻止z3生成空模型。 [∃v, v1 : v = v1]就是這樣一個例子。例如，如果我們將這樣的公式添加到求解器中，然後嘗試創建類似於allsat過程的東西（添加越來越多的約束以排除越來越多的模型），那麼在獲得空模型之前，我們會遇到不合適的情況。

那麼，請您介紹一下任何描述z3如何處理量詞和空模型的文檔/論文？ 另外，如果我選擇僅限於非空模型，請問z3的正確方法是什麼？像[∃v, v1 : v = v1]這樣的東西似乎可以做到這一點，但有沒有更好的辦法？

Answer 1

Z3不考慮空模型。這是一階邏輯中的一個標準假設。欲瞭解更多詳情，請搜索「一階邏輯空模型」，您將獲得許多解釋此慣例動機的鏈接。 wikipedia page for first-order logic有一個簡要說明（「空域」部分）。

此外，我們不應該混淆[]與空模型。它只是說爲了滿足輸入公式，Z3不需要爲輸入公式中任何未解釋的符號分配解釋。 Z3只顯示滿足公式所需符號的解釋。例如，公式[∃v : v = v]不包含任何未解釋的符號，則Z3僅顯示空分配[]。