定義自定義量詞

Question

我試圖讓Z3驗證一些在表示法中使用迭代最大值的形式證明。例如，對於fa函​​數（↑i：  0≤i < N：  f（i））將f應用於0和N之間的值時指定f的最高值。它可以很好地公理化：

（↑I：p（I）表示：f（i））的 ≤  X     < =>    （∀i：  p（I）：  F（1）≤x）的

與對於我的類型來說謂詞是謂詞。有沒有辦法在Z3中定義這樣的量詞？

這是非常方便的制定我的證明，所以我想保持儘可能接近這個定義。

謝謝！

Answer 1

在Z3中沒有直接的方法來定義這種活頁夾。 Z3基於經典的簡單排序的一階邏輯，其中唯一的結合物是通用的和潛在的量化。特別是，Z3不會讓你直接編寫lambda表達式。使用包含嵌套粘合劑的Z3來證明定理的一種方法是首先應用拉姆達提升，然後試圖證明所得到的一階公式。

在你的例子中，你想定義一個常量max_p_f。 具有以下屬性：

forall i: p(i) => max_p_f >= f(i) 
(exists i: p(i) & max_p_f = f(i)) or (forall i . not p(i)) 

說（假設確界定義的域等） 你將不得不爲每一個P，F組合常量要應用的最大功能。

定義這樣的函數是高級邏輯證明助手的標準。 當將證明義務映射到一階後端（E，Vampire，Z3等）時，Isabelle定理證明器應用類似於上述的變換。