與Z3可能的錯誤：Z3是不能證明一個定理的拓撲

我正在翻譯使用給定的有代碼給一般的拓撲結構定理以下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

請在線運行此示例here

第一個sat是正確的;但第二個sat是錯誤的，它必須是unsat。換句話說，Z3說這個定理和它的否定是同時存在的。

請讓我知道在這種情況下會發生什麼。非常感謝。祝一切順利。

來源

2014-04-12 Juan Ospina

公式的否定和公式的否定可能與背景理論T相一致。特別是，當T不完整時，則存在既不是T的後果也不符合T的句子在你的情況下，理論T是拓撲公理的集合。您可以使用命令（get-model）來獲得滿足公理和句子的模型。

來源

2014-04-14 16:33:06

非常感謝您的回答，但根據TPTP網站，公理導致定理沒有麻煩。我正在嘗試其他定理，但Z3會產生一個「超時」。我在想，Z3不能證明這樣的定理。你同意嗎？。從另一方面來說，當使用命令（get-model）時，由Z3生成的模型是微不足道的。當我試圖獲得一個不平凡的模型Z3再次產生「超時」。非常感謝，並一切順利。 –

與Z3可能的錯誤：Z3是不能證明一個定理的拓撲

回答

相關問題