如何用Z3-SMT-LIB证明Z3群满足结合律 [英] How to prove that the Z3 group satisfies the associative law using Z3-SMT-LIB

问题描述

我正在尝试使用以下 Z3-SMT-LIB 代码证明 Z3 群满足结合律

I am trying to prove that the Z3 group satisfies the associative law using the following Z3-SMT-LIB code

(set-option :mbqi true)
(declare-sort S)
(declare-fun f (S S) S)
(declare-const a S)
(declare-const b S)
(declare-const c S)
(assert (forall ((x S) (y S))
            (= (f x y)  (f y x))))
(assert (forall ((x S))
            (= (f x a) x)))
(assert (= (f b b) c))
(assert (= (f b c) a))
(assert (= (f c c) b))
(check-sat)
(get-model)
(declare-fun x () S)
(declare-fun y () S)
(declare-fun z () S)
(assert (not (=> (and (or (= x a) (= x b) (= x c)) (or (= y a) (= y b) (= y c)) 
                  (or (= z a) (= z b) (= z c))) 
            (=  (f x (f y z)) (f (f x y) z)))))
(check-sat)  

对应的输出为

sat 
(model 
;; universe for S: 
;; S!val!1 S!val!0 S!val!2 
;; ----------- 
;; definitions for universe elements: 
(declare-fun S!val!1 () 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!0) (= x S!val!2))) 
;; ----------- 
(define-fun b () S S!val!0) 
(define-fun c () S S!val!1) 
(define-fun a () S 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!1) (= x!2 S!val!1)) S!val!0 
  (ite (and (= x!1 S!val!1) (= x!2 S!val!0)) S!val!2 
  (ite (and (= x!1 S!val!0) (= x!2 S!val!2)) S!val!0 
  (ite (and (= x!1 S!val!2) (= x!2 S!val!0)) S!val!0 
  (ite (and (= x!1 S!val!2) (= x!2 S!val!1)) S!val!1 
  (ite (and (= x!1 S!val!1) (= x!2 S!val!2)) S!val!1 x!1))))))))) 
 ) 

 unsat

在线运行此示例此处

问题是:

1. 这个证明是否正确?

1. Is this proof correct?

有更优雅的证明吗?

推荐答案

每个组都必须满足结合公理.我猜你想证明第一个断言块的每个模型都满足结合性公理.为了完成这个例子，我们还应该证明逆元公理.

Every group must satisfy the associativity axiom. I guess you are trying to prove that every model for the first block of assertions satisfy the associativity axiom. To complete the example, we should also prove the inverse element axiom.

为了证明这两个性质，我们可以使用以下命令:

To prove these two properties, we can use the following commands:

(push)
;; prove the inverse axiom
(assert (not (forall ((x S)) (exists ((y S)) (= (f x y) a)))))
(check-sat)                
(pop)

(push)
;; prove the associativity axiom
(assert (not (forall ((x S) (y S) (z S)) (= (f x (f y z)) (f (f x y) z)))))
(check-sat)                
(pop)

Z3 无法证明它们.然而，如果我们断言我们只对大小最多为 3 的模型感兴趣，它就成功了.

Z3 cannot prove them. However, it succeeds if we assert that that we are only interested in models of size at most 3.

(assert (forall ((x S)) (or (= x a) (= x b) (= x c))))

这里是完整示例.

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