Определение пользовательских квантификаторов

Я пытаюсь заставить Z3 проверить некоторые формальные доказательства, использующие повторяющийся максимум в обозначениях. Например, для f функция (↑i: 0 ≤ i ‹ N: f(i)) обозначает наибольшее значение f, когда она применяется к значению между 0 и N. Ее можно красиво аксиоматизировать с помощью:

(↑i: p(i): f(i)) ≤ x ‹=> (∀i: p(i): f(i) ≤ x)

с p предикатом над типом i. Есть ли способ определить такой квантификатор в Z3?

Оно весьма удобно для формулировки моих доказательств, поэтому я хотел бы максимально приблизить его к этому определению.

Спасибо!


z3 quantifiers
person simon1505475    schedule 06.07.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

В Z3 нет прямого способа определить такие биндеры. Z3 основан на классической логике первого порядка с простой сортировкой, где единственными связующими элементами являются универсальная и экзистенциальная квантификация. В частности, Z3 не позволяет напрямую писать лямбда-выражения. Один из подходов к доказательству теорем с использованием Z3, включающих вложенные связыватели, состоит в том, чтобы сначала применить лямбда-лифтинг, а затем попытаться доказать результирующую формулировку первого порядка.

В вашем примере вы хотите определить константу max_p_f. Со следующими свойствами:

forall i: p(i) => max_p_f >= f(i)
(exists i: p(i) & max_p_f = f(i)) or (forall i . not p(i))

скажем (при условии, что супремум определен в домене и т. д.). Вам нужно будет создать константы для каждой комбинации p, f, где вы хотите применить функцию max.

Определение таких функций является стандартным в помощниках по доказательству для логики высшего порядка. Доказательство теоремы Изабель применяет преобразования, подобные описанным выше, при сопоставлении обязательств по доказательству с бэкендами первого порядка (E, Vampire, Z3 и т. д.).

person Nikolaj Bjorner    schedule 06.07.2012
comment
Благодарю вас! Я посмотрю, что я могу сделать с этим! - person simon1505475; 07.07.2012