Z3中的parthood定义

我试图在 Z3 中定义集合对（使用数组定义）之间的部分关系（在下面的代码中称为 C）。 我写了 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 不会返回未知。如果我考虑无反对称性的自反性和传递性，情况也是如此。

量词本质上是不完整的。因此，Z3（或任何其他 SMT 求解器）回归也就不足为奇了unknown当他们在场时。求解器使用一些启发式方法来处理量词，例如电子匹配；但这些仅在您有基本术语时才适用。你的公式只有量化的公理，不太可能从中受益。

对于一般量词的推理，SMT 求解器根本不是最佳选择；为此使用定理证明器（Isabelle、Lean、Coq 等）。

这是 Leonardo 制作的关于在 SMT 求解中使用量词的精彩幻灯片：https://leodemoura.github.io/files/qsmt.pdf https://leodemoura.github.io/files/qsmt.pdf。它可以帮助您进一步了解相关技术和困难。