Использование Z3Py в Интернете, чтобы доказать, что п^5 <= 5^при п> = 5

Question

Используя следующий код:

n = Int('n') 
s = Solver() 
s.add(n >= 5) 
s.add(Not(n**5 <= 5**n)) 
print s 
print s.check() 

мы получаем следующий результат:

[n ≥ 5, ¬(n^5 ≤ 5^n)] 
unknown 

Он должен скажем, что Z3Py не может дать прямого доказательства.

Теперь, используя код

n = Int('n') 
prove(Implies(n >= 5, n**5 <= 5**n)) 

Z3Py также терпит неудачу.

Возможное косвенное доказательство заключается в следующем:

n = Int('n') 
e, f = Ints('e f') 
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True) 
prove(Implies(And(e >=0, f >= 0), t >= 0)) 

и выход:

proved 

доказательство с помощью Isabelle + Maple дается в: теоремы и алгоритмы: Интерфейс между Изабеллой и Maple. Клеменс Балларин. Карстен Хоманн. Жак Калмет.

Другие возможные косвенные доказательства использования Z3Py выглядит следующим образом:

n = Int('n') 
e, f = Ints('e f') 
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True) 
s = Solver() 
s.add(e >= 0, f >= 0) 
s.add(Not(t >= 0)) 
print s 
print s.check() 

и выход:

[e ≥ 0, 
f ≥ 0, 
¬(7849 + 
9145·f + 
4090·f·f + 
890·f·f·f + 
95·f·f·f·f + 
4·f·f·f·f·f + 
5·e ≥ 
0)] 
unsat 

Пожалуйста, дайте мне знать, если это возможно, чтобы иметь более прямое доказательство с помощью Z3Py. Большое спасибо.

Answer 1

Z3 имеет очень ограниченную поддержку нелинейной целочисленной арифметики. См следующей соответствующей должности для получения дополнительной информации:

• How does Z3 handle non-linear integer arithmetic?

Z3 имеет полный решатель (nlsat) для нелинейной реальной (полиномиальной) арифметики. Вы можете упростить свой сценарий, написав

Z3 использует nlsat в задаче выше, потому что содержит только реальные переменные. Мы также можем заставить Z3 использовать nlsat, даже если проблема содержит целочисленные переменные.

n = Int('n') 
e, f = Ints('e f') 
s = Tactic('qfnra-nlsat').solver() 
s.add(e >= 0, f >= 0) 
s.add(Not(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5 >= 0)) 
print s 
print s.check()