Какие дополнительные аксиомы нам нужно добавить, чтобы Z3 мог проверять выполнимость программ с повторениями?

Как мы знаем, Z3 имеет ограничения с рецидивами. Есть ли способ получить результат для следующей программы? какое дополнительное уравнение поможет z3 получить результат?

    from z3 import *
    ackermann=Function('ackermann',IntSort(),IntSort(),IntSort())
    m=Int('m')
    n=Int('n')
    s=Solver()
    s.add(ForAll([n,m],Implies(And(n>=0,m>=0),ackermann(m,n) == If(m!=0,If(n!=0,ackermann(m - 1,ackermann(m,n - 1)),If(n==0,ackermann(m - 1,1),If(m==0,n + 1,0))),If(m==0,n + 1,0)))))
    s.add(n>=0)
    s.add(m>=0)
    s.add(Not(Implies(ackermann(m,n)>=0,ackermann(m+1,0)>=0)))
    s.check()

z3 smt z3py
person Tom    schedule 10.07.2017    source источник

Ответы (2)


arrow_upward
1
arrow_downward

Z3 не будет пытаться делать что-либо по индукции для вас, но (как упомянул Левент Эркок) вы можете дать ему гипотезу индукции и проверить, следует ли результат.

Это работает на вашем примере следующим образом.

(declare-fun ackermann (Int Int) Int)

(assert (forall ((m Int) (n Int))
                (= (ackermann m n)
                   (ite (= m 0) (+ n 1)
                        (ite (= n 0) (ackermann (- m 1) 1)
                             (ackermann (- m 1) (ackermann m (- n 1))))))))

(declare-const m Int)
(declare-const n Int)

(assert (>= m 0))
(assert (>= n 0))

; Here's the induction hypothesis
(assert (forall ((ihm Int) (ihn Int))
                (=> (and (<= 0 ihm) (<= 0 ihn)
                         (or (< ihm m) (and (= ihm m) (< ihn n))))
                    (>= (ackermann ihm ihn) 0))))

(assert (not (>= (ackermann m n) 0)))
(check-sat) ; reports unsat as desired
person James Wilcox    schedule 27.08.2017

arrow_upward
2
arrow_downward

С вложенным рекурсивным определением, таким как функция Аккермана, я не думаю, что вы можете многое сделать, чтобы убедить Z3 (или любой другой SMT-решатель) действительно делать какие-либо интересные доказательства. Такие свойства потребуют умных индуктивных аргументов, и SMT-решатель просто не подходит для такого рода проверки. Доказательство теорем, такое как Isabelle, HOL, Coq, ..., является лучшим выбором здесь.

Сказав это, основной подход к установлению свойств рекурсивных функций в SMT состоит в том, чтобы буквально закодировать индуктивную гипотезу как количественную аксиому и организовать так, чтобы свойство, которое вы хотите доказать, точно соответствовало этой аксиоме, когда механизм электронного сопоставления срабатывает. поэтому он может "правильно" создавать экземпляры квантификаторов. Я беру здесь слово правильно в кавычки, потому что механизм сопоставления будет работать дальше и будет продолжать реализовывать аксиому непродуктивным образом, особенно для такой функции, как функция Аккермана. Доказывающие теоремы, с другой стороны, точно дают вам контроль над структурой доказательства, так что вы можете явно направлять доказывающего через пространство поиска доказательства.

Вот пример, который вы можете посмотреть: список concat в z3, который выполняет индуктивное доказательство гораздо более простое индуктивное свойство, чем вы нацеливаете, используя интерфейс SMT-Lib. Хотя будет непросто расширить его для обработки вашего конкретного примера, он может дать некоторое представление о том, как это сделать.

В конкретном случае Z3 вы также можете использовать его механизм рассуждений с фиксированной точкой, используя алгоритм PDR, чтобы отвечать на запросы об определенных рекурсивных функциях. См. http://rise4fun.com/z3/tutorialcontent/fixedpoints#h22 для пример, который показывает, как смоделировать знаменитую функцию 91 Маккарти в качестве интересного тематического исследования.

person alias    schedule 11.07.2017