Как использовать 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 является обновленным примером с этой командной последовательностью.