parthood definition in Z3

Question

저는 Z3에서 (배열을 사용하여 정의 된) 쌍 쌍 사이의 부분 관계 (아래 코드에서 C라고 함)를 정의하려고합니다. 반사성, transitivity 및 antisymmetry를 정의하는 3 assert를 썼지 만 Z3은 "unknown"을 반환하고 나는 그 이유를 이해하지 못합니다.

(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을 반환한다는 것은 놀라운 일이 아닙니다. e-matching과 같은 한정어 처리에 사용되는 몇 가지 발견 적 방법이 있습니다. 그러나 그것들은 주변 용어를 사용하는 경우에만 적용됩니다. 정량화 된 공리만을 가진 당신의 공식은 그로부터 이익을 얻지 못할 것입니다.

일반적으로 한정 기호에 대한 이유 때문에 SMT 솔버가 최선의 선택이 아닙니다. 정리 프로버 (Isabelle, Lean, Coq 등)를 사용하십시오.

다음은 Leonardo가 SMT 해결에서 수량 기호를 사용하는 멋진 슬라이드 데크입니다 : https://leodemoura.github.io/files/qsmt.pdf. 그것은 관련 기술과 어려움에 대한 더 깊은 통찰력을 제공 할 수 있습니다.