如何使用 Z3 SMT-LIB 证明 D3 群的定理 [英] How to use Z3 SMT-LIB to prove theorems for the group D3

问题描述

D3 组的产品表是:

使用以下 Z3 SMT-LIB 代码可以获得一个表示:

Using the following Z3 SMT-LIB code is possible to obtain a representation:

(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 给出逆.对应的输出为:

In this code the function f gives the product and the function g gives the inverse. The corresponding output is:

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))))))))))))))))))))))))))) 
 )

使用这种表示可以证明以下定理:

Using this representation is possible to prove the following theorem:

证明是:

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

输出

S!val!1 
S!val!1

在此处运行完整代码

问题是:有没有可能得到这个定理的更优雅的证明?

The question is: It is possible to get a more elegant proof of this theorem?

推荐答案

您要检查断言是否暗示 (f (f R3 R1) (g R3)) 和 R2 是相等的.你可以通过显示上面的断言加上断言来实现这一点

You want to check whether the assertions imply that (f (f R3 R1) (g R3)) and R2 are equal. You can accomplish that by showing that the the assertions above plus the assertion

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

不满意.您可以在 (check-sat) 之前添加以下附加断言.这里是更新的示例.

are unsatisfiable. You can add the following additional assertion before the (check-sat). Here is the updated example.

您也可以在原始断言集之后使用以下命令序列

You may also use the following command sequence after your original set of assertions

    (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 is the updated example with this command sequence.

这篇关于如何使用 Z3 SMT-LIB 证明 D3 群的定理的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！