Z3中的部分定義

Question

我試圖在Z3中定義成對關係（在下面的代碼中稱爲C）（使用數組定義）之間的parthood關係。 我寫了3個斷言來定義反身性，傳遞性和反對稱性，但Z3返回「未知」，我不明白爲什麼。

(define-sort Set() (Array Int Bool)) 
(declare-rel C (Set Set)) 

; reflexivity 
(assert (forall ((X Set)) (C X X))) 

; transitive 
(assert (forall ((X Set)(Y Set)(Z Set)) 
    (=> 
     (and (C X Y) (C Y Z)) 
     (C X Z) 
    ) 
)) 

; antisymmetric 
(assert (forall ((X Set)(Y Set)) 
    (=> 
     (and (C X Y) (C Y X)) 
     (= X Y) 
    ) 
)) 

(check-sat) 

我注意到，當反對稱性被認爲是與其他2一個斷言未知僅返回。如果我只考慮反對稱性Z3不會返回未知數。如果我考慮沒有反對稱性的反身性和傳遞性，那也是一樣的。

Answer 1

量詞本質上是不完整的。所以，Z3（或任何其他SMT解算器）在出現時會返回unknown也就不足爲奇了。有幾種啓發式算法用於處理量詞，例如電子匹配;但這些只會在你有地面條件時適用。你的公式只有量化公理，不太可能從中受益。

有關一般量詞推理，一個SMT求解器根本就不是最好的選擇;使用定理證明（Isabelle，Lean，Coq等）。

這裏是一個不錯的幻燈片平臺由萊昂納多在SMT解決使用量詞：https://leodemoura.github.io/files/qsmt.pdf。它可以幫助進一步瞭解相關技術和困難。