Когда формула в Z3 является unsat и (get-proof) указана, есть выход, который я не нахожу никакой информации о том, что это такое. Где я могу найти документацию об этом?Результат контрпримера Z3
Кажется, что я не читаю, есть ли какой-нибудь инструмент, который воспринимает это как вход?
Приветствия, Matt
The "доказательства", произведенные Z3 не для потребления человеком. Устаревшая версия формата описана в статье: Proofs and Refutations, and Z3. Файл z3_api.h имеет длинное описание каждого из правил доказательства. Идентификаторы правила проверки начинаются с Z3_OP_PR. Я знаю о двух приложениях, которые используют объекты Z3 proof. Следующие документы содержат множество примеров и описывают, как можно использовать объекты доказательства.
1- Изабелла Интерактивная теорема о теореме: доказательства Z3 реконструируются внутри Изабель с использованием доверенного ядра. Вы можете найти несколько статей, описывающих эту работу и стойкую формат Z3 в Sascha Bohme's homepage
Как сказал подушечка, unsat-cores намного проще в использовании.
Большое спасибо за ваши ссылки. Я рассмотрю оба метода. Так что благодаря @pad! – MattKay
Команда '(get-unsat-core)' кажется, что вы хотите. Официальный пример: http://rise4fun.com/Z3/smtc_core – pad