Как обнаружить или доказать рекуррентные отношения периодических последовательностей с помощью Z3?

Возможно

(declare-fun f (Int Int) Int)

(assert (forall ((a Int)) (= (f 0 a) 0)))
(assert (forall ((x Int) (a Int)) (=> (and (>= x 0) (>= a 0) (> (f x a) a)) (= (f (+ x 1) a) (- (f x a) 1)))))
(assert (forall ((x Int) (a Int)) (=> (and (>= x 0) (>= a 0) (<= (f x a) a)) (= (f (+ x 1) a) (+ (f x a) 1)))))
(assert (forall ((x Int) (y Int) (a Int)) (=> (and (>= x 0) (> y x) (>= a 0)) (not (= (f x a) (f y a))))))
(check-sat)

хотя это не говорит о периодичности f.

Пожалуйста, всегда включайте полный код в свои образцы; поскольку то, что вы дали, не является действительным кодом, который люди должны запускать и наблюдать.

Предполагая, что ваш код на самом деле следующий:

from z3 import *
s=Solver()
A=Int('A')
n=Int('n')
k=Int('k')
y4 = Function('f', IntSort(), IntSort())
s.add(A>0)
s.add(ForAll([n],Implies(n>=0,y4(n + 1) == If(y4(n)<=A,y4(n) + 1,y4(n)-1))))
s.add(y4(0) == 0)
s.add(Not(ForAll([n],Exists([k],Implies(And(k>0,n>=0),y4(n)==y4(n+k))))))

Вы можете увидеть, что производит Z3, добавив:

print s.sexpr()
print s.check()

Если вы запустите этот скрипт, вы получите:

(declare-fun A () Int)
(declare-fun f (Int) Int)
(assert (> A 0))
(assert (forall ((n Int))
  (let ((a!1 (= (f (+ n 1)) (ite (<= (f n) A) (+ (f n) 1) (- (f n) 1)))))
    (=> (>= n 0) a!1))))
(assert (= (f 0) 0))
(assert (let ((a!1 (forall ((n Int))
             (exists ((k Int))
               (=> (and (> k 0) (>= n 0)) (= (f n) (f (+ n k))))))))
  (not a!1)))

unsat

И вы можете увидеть проблему; ваше последнее утверждение гласит, что существует n, такое, что для всех k периодичность не выполняется. (Поскольку вы поместили оболочку Not.) Ясно, что это unsat.

В несколько более идиоматическом Z3 я бы закодировал вашу проблему следующим образом:

from z3 import *

s = Solver ()

A = Int ('A')
s.add(A > 0)

f = Function('f', IntSort(), IntSort())
x = Int ('x')

s.add(f(0) == 0)
s.add(ForAll(x, Implies(x >= 0, f(x + 1) == If(A >= f(x), f(x)+1, f(x)-1))))

k = Int('k')
s.add(ForAll(x, Exists(k, f(x+k) == f(x))))

print s.sexpr()
print s.check()

Но ожидать, что Z3 это докажет, было бы наивно. Действительно, когда я его запускаю, я получаю:

(declare-fun A () Int)
(declare-fun f (Int) Int)
(assert (> A 0))
(assert (= (f 0) 0))
(assert (forall ((x Int))
  (let ((a!1 (= (f (+ x 1)) (ite (>= A (f x)) (+ (f x) 1) (- (f x) 1)))))
    (=> (>= x 0) a!1))))
(assert (forall ((x Int)) (exists ((k Int)) (= (f (+ x k)) (f x)))))

 [Ctrl-C]

В данном случае моделирование кажется мне правильным, но Z3 не отвечает, поэтому мне пришлось нажать Ctrl-C, чтобы остановить его через некоторое время.

Но хорошо то, что вы можете взять этот SMTLib и поместить его в файл, прикрепить в конце (check-sat) и запустить Z3 следующим образом:

z3 -v:10 a.smt2 a.smt2

И он напечатает вам много шагов о том, что он делает. Я предполагаю, что он теряется в процессе создания экземпляра квантификатора. Типичное решение - предоставить шаблоны кванторов, но мне не ясно, какими они будут в этом случае. Здесь есть несколько примеров http://ericpony.github.io/z3py-tutorial/advanced-examples.htm, который может помочь.