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。它可以帮助进一步了解相关技术和困难。