Возможная ошибка с Z3: Z3 не может доказать теорему в топологии

Я пытаюсь доказать с помощью Z3 теорему общей топологии, изложенную в

Топология TPTP

Я перевожу приведенный там код, используя следующий код 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

Запустите этот пример онлайн здесь

Первый sat правильный; но второй sat неправильный, он должен быть unsat. Другими словами, Z3 говорит, что теорема и ее отрицание верны одновременно.

Пожалуйста, дайте мне знать, что происходит в этом случае. Большое спасибо. Всего наилучшего.


topology z3 z3py theorem-proving
person Juan Ospina    schedule 12.04.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Возможно, что и формула, и отрицание формулы непротиворечивы по отношению к фоновой теории Т. В частности, когда Т не является полным, то есть предложения, которые не являются ни следствием Т, ни несовместимыми с Т. В вашем случае теория T есть множество аксиом топологии. Вы можете использовать команду (get-model), чтобы получить модель, удовлетворяющую аксиомам и предложению.

person Nikolaj Bjorner    schedule 14.04.2014
comment
Большое спасибо за ваш ответ, но, согласно веб-сайту TPTP, аксиомы без проблем приводят к теореме. Я пытаюсь использовать другие теоремы, но Z3 выдает тайм-аут. Я думаю, что Z3 не в состоянии доказать такие теоремы. Ты согласен?. С другой стороны, при использовании команды (get-model) модель, сгенерированная Z3, тривиальна. Когда я пытаюсь получить нетривиальную модель, Z3 снова генерирует тайм-аут. Большое спасибо и всего наилучшего. - person Juan Ospina; 14.04.2014