Using (set-option :qi-eager-threshold 70000)
suggested by Leonardo de Moura, Z3 is able to prove the theorem until n = 60000 (locally, online until n = 10000).
How to make bounded inductive proof of a certain general theorem in Group Theory
-
07-10-2022 - |
문제
I am trying to proof by induction that:
Given a group G then forall(x,y,z) / ((y^n)x(z^n) = x) => (Order(G) = n)
I am using bounded induction with the following code
;; Derive order n from a single axiom for groups order n.
;; ((Y^n)X(Z^n) = X )=> (order(G) = n) for 1 < n < 23
(declare-sort S)
(declare-fun e () S)
(declare-fun mult (S S) S)
(declare-fun power (S Int) S)
(assert (forall ((x S)) (= e (power x 0))))
(assert (forall ((x S)) (= x (power x 1))))
(assert (forall ((n Int) (x S))
(=> (and (>= n 2) (<= n 22))
(= (power x n) (mult x (power x (- n 1)))))))
(assert (= (mult e e) e))
(check-sat)
(define-fun p ((x S) (y S) (z S) (w S) (n Int)) Bool
(=> (= (mult (power y n) (mult x (power z n)))
x) (= (power w n) e) ) )
(assert (forall ((x S) (y S) (z S) (w S)) (p x y z w 2)))
(assert (forall ((x S) (y S) (z S) (w S) (n Int))
(=> (and (> n 2) (<= n 22))
(= (p x y z w n) (p x y z w (- n 1))))))
;; Bounded inductive proof.
(assert (not (forall ((x S) (y S) (z S) (w S)) (p x y z w 22))))
(check-sat)
And the output is the expected:
sat
unsat
Run this code online here
I am proving the theorem for 2 < n < 23. When I try with 2 < n < 24 I am obtaining "timeout".
The question is: How to go beyond n=22 in this proof ?
해결책
제휴하지 않습니다 StackOverflow