가능한 버그 : Z3는 토폴로지

Question

내가 Z3와

TPTP-Topology

내가 사용이 주어진 코드를 번역시에 주어진 일반적인 토폴로지의 정리를 증명하기 위해 노력하고

을의 정리를 증명 할 수 없습니다 Z3-SMT-LIB 코드 다음

;; File  : TOP001-2 : TPTP v6.0.0. Released v1.0.0. 
;; Domain : Topology 
;; Problem : Topology generated by a basis forms a topological space, part 1 

(declare-sort S) 
(declare-sort Q) 
(declare-sort P) 

(declare-fun elemcoll (S Q) Bool) 
(declare-fun elemset (P S) Bool) 
(declare-fun unionmemb (Q) S) 

(declare-fun f1 (Q P) S) 

(declare-fun f11 (Q S) P) 
(declare-fun basis (S Q) Bool) 
(declare-fun Subset (S S) Bool) 
(declare-fun topbasis (Q) Q) 

;; union of members axiom 1. 
(assert (forall ((U P) (Vf Q)) (or (not (elemset U (unionmemb Vf))) 
            (elemset U (f1 Vf U))) )) 
;; union of members axiom 2. 

(assert (forall ((U P) (Vf Q)) (or (not (elemset U (unionmemb Vf))) 
            (elemcoll (f1 Vf U) Vf)) )) 


;; basis for topology, axiom 28 

(assert (forall ((X S) (Vf Q)) (or (not (basis X Vf)) (= (unionmemb Vf) X) ) )) 

;; Topology generated by a basis, axiom 40. 

(assert (forall ((Vf Q) (U S)) (or (elemcoll U (topbasis Vf)) 
           (elemset (f11 Vf U) U)) )) 

;; Set theory, axiom 7. 

(assert (forall ((X S) (Y Q)) (or (not (elemcoll X Y)) (Subset X (unionmemb Y))) )) 

;; Set theory, axiom 8. 
(assert (forall ((X S) (Y S) (U P)) (or (not (Subset X Y)) (not (elemset U X)) 
                   (elemset U Y) ))) 

;; Set theory, axiom 9. 
(assert (forall ((X S)) (Subset X X) )) 

;; Set theory, axiom 10. 
(assert (forall ((X S) (Y S) (Z S)) (or (not (= X Y)) (not (Subset Z X)) (Subset Z Y)) )) 

;; Set theory, axiom 11. 
(assert (forall ((X S) (Y S) (Z S)) (or (not (= X Y)) (not (Subset X Z)) (Subset Y Z)) )) 

(check-sat) 

(push) 
(declare-fun cx() S) 
(declare-fun f() Q) 
(assert (basis cx f)) 
(assert (not (elemcoll cx (topbasis f)))) 
(check-sat) 
(pop) 

(push) 
(assert (basis cx f)) 
(assert (elemcoll cx (topbasis f))) 
(check-sat) 
(pop) 

해당 출력은

sat 
sat 
sat 

인 0

이 예제를 온라인으로 실행하십시오. here

첫 번째 sat은 올 바릅니다. 두 번째 sat이 잘못 되었으면 unsat이어야합니다. 즉, Z3은 정리와 그 부정이 동시에 진실이라고 말합니다.

이 경우 어떻게되는지 알려주세요. 많은 감사합니다. 모두 제일 좋다.

Answer 1

수식과 수식의 부정은 배경 이론 T와 일치 할 수 있습니다. 특히 T가 완료되지 않은 경우 T의 결과도 T와 일치하지도 않는 문장이 있습니다. 당신의 경우 이론 T는 토폴로지 공리 (topology axioms)의 집합입니다. 명령 (get-model)을 사용하여 공리와 문장을 만족하는 모델을 얻을 수 있습니다.