如何使用Z3 SMT-LIB證明定理爲組D3

Question

的產品爲基的表D3是：

採用下述Z3 SMT-LIB代碼可能獲得的表示：

(set-option :mbqi true) 
(declare-sort S) 
(declare-fun f (S S) S) 
(declare-fun g (S) S) 
(declare-const E S) 
(declare-const R1 S) 
(declare-const R2 S) 
(declare-const R3 S) 
(declare-const R4 S) 
(declare-const R5 S) 
(assert (forall ((x S)) 
      (= (f x E) x))) 
(assert (forall ((x S)) 
      (= (f E x) x)))    
(assert (= (f R1 R1) R2)) 
(assert (= (f R1 R2) E)) 
(assert (= (f R1 R3) R4)) 
(assert (= (f R1 R4) R5)) 
(assert (= (f R1 R5) R3)) 
(assert (= (f R2 R1) E)) 
(assert (= (f R2 R2) R1)) 
(assert (= (f R2 R3) R5)) 
(assert (= (f R2 R4) R3)) 
(assert (= (f R2 R5) R4)) 
(assert (= (f R3 R1) R5)) 
(assert (= (f R3 R2) R4)) 
(assert (= (f R3 R3) E)) 
(assert (= (f R3 R4) R2)) 
(assert (= (f R3 R5) R1)) 
(assert (= (f R4 R1) R3)) 
(assert (= (f R4 R2) R5)) 
(assert (= (f R4 R3) R1)) 
(assert (= (f R4 R4) E)) 
(assert (= (f R4 R5) R2)) 
(assert (= (f R5 R1) R4)) 
(assert (= (f R5 R2) R3)) 
(assert (= (f R5 R3) R2)) 
(assert (= (f R5 R4) R1)) 
(assert (= (f R5 R5) E)) 
(assert (= (g E) E)) 
(assert (= (g R1) R2)) 
(assert (= (g R2) R1)) 
(assert (= (g R3) R3)) 
(assert (= (g R4) R4)) 
(assert (= (g R5) R5)) 
(check-sat) 
(get-model) 

在該代碼中的函數f給出了產品和功能g給出逆。相應的輸出是：

sat 
(model 
;; universe for S: 
;; S!val!1 S!val!3 S!val!5 S!val!4 S!val!0 S!val!2 
;; ----------- 
;; definitions for universe elements: 
(declare-fun S!val!1() S) 
(declare-fun S!val!3() S) 
(declare-fun S!val!5() S) 
(declare-fun S!val!4() S) 
(declare-fun S!val!0() S) 
(declare-fun S!val!2() S) 
;; cardinality constraint: 
(forall ((x S)) (or (= x S!val!1) (= x 
    S!val!3) (= x S!val!5) (= x S!val!4) (= x S!val!0) (= x S!val!2))) 
;; ----------- 
(define-fun R1() S S!val!0) 
(define-fun R3() S S!val!3) 
(define-fun R2() S S!val!1) 
(define-fun R4() S S!val!4) 
(define-fun R5() S S!val!5) 
(define-fun E() S S!val!2) 
(define-fun g ((x!1 S)) S 
(ite (= x!1 S!val!0) S!val!1 
(ite (= x!1 S!val!1) S!val!0 
(ite (= x!1 S!val!3) S!val!3 
(ite (= x!1 S!val!4) S!val!4 
(ite (= x!1 S!val!5) S!val!5 S!val!2)))))) 
(define-fun f ((x!1 S) (x!2 S)) S 
(ite (and (= x!1 S!val!0) (= x!2 S!val!0)) S!val!1 
(ite (and (= x!1 S!val!0) (= x!2 S!val!1)) S!val!2 
(ite (and (= x!1 S!val!0) (= x!2 S!val!3)) S!val!4 
(ite (and (= x!1 S!val!0) (= x!2 S!val!4)) S!val!5 
(ite (and (= x!1 S!val!0) (= x!2 S!val!5)) S!val!3 
(ite (and (= x!1 S!val!1) (= x!2 S!val!0)) S!val!2 
(ite (and (= x!1 S!val!1) (= x!2 S!val!1)) S!val!0 
(ite (and (= x!1 S!val!1) (= x!2 S!val!3)) S!val!5 
(ite (and (= x!1 S!val!1) (= x!2 S!val!4)) S!val!3 
(ite (and (= x!1 S!val!1) (= x!2 S!val!5)) S!val!4 
(ite (and (= x!1 S!val!3) (= x!2 S!val!0)) S!val!5 
(ite (and (= x!1 S!val!3) (= x!2 S!val!1)) S!val!4 
(ite (and (= x!1 S!val!3) (= x!2 S!val!3)) S!val!2 
(ite (and (= x!1 S!val!3) (= x!2 S!val!4)) S!val!1 
(ite (and (= x!1 S!val!3) (= x!2 S!val!5)) S!val!0 
(ite (and (= x!1 S!val!4) (= x!2 S!val!0)) S!val!3 
(ite (and (= x!1 S!val!4) (= x!2 S!val!1)) S!val!5 
(ite (and (= x!1 S!val!4) (= x!2 S!val!3)) S!val!0 
(ite (and (= x!1 S!val!4) (= x!2 S!val!4)) S!val!2 
(ite (and (= x!1 S!val!4) (= x!2 S!val!5)) S!val!1 
(ite (and (= x!1 S!val!5) (= x!2 S!val!0)) S!val!4 
(ite (and (= x!1 S!val!5) (= x!2 S!val!1)) S!val!3 
(ite (and (= x!1 S!val!5) (= x!2 S!val!3)) S!val!1 
(ite (and (= x!1 S!val!5) (= x!2 S!val!4)) S!val!0 
(ite (and (= x!1 S!val!5) (= x!2 S!val!5)) S!val!2 
(ite (= x!1 S!val!2) x!2 x!1))))))))))))))))))))))))))) 
) 

使用這種表示可以證明以下定理：

證據是：

(eval (f (f R3 R1) (g R3))) 
(eval R2) 

與輸出

S!val!1 
S!val!1 

運行完整代碼here

問題是：可以得到這個定理的更優雅的證明嗎？

Answer 1

你想檢查斷言暗示(f (f R3 R1) (g R3))和R2是否相等。您可以通過顯示以上斷言加上斷言來實現該目的。

(assert (not (= (f (f R3 R1) (g R3)) R2))) 

是不令人滿意的。 您可以在(check-sat)之前添加以下附加斷言。 Here是更新的示例。

您也可以使用下面的命令序列原始的斷言集合後

(check-sat) ; check if the set of assertions is consistent 
    (get-model) ; display the model 
    ; assert the negation of the conjecture 
    (assert (not (= (f (f R3 R1) (g R3)) R2))) 
    (check-sat) 

Here是更新的例子使用此命令序列。