Контрпример вывода Z3 - PullRequest
Новая
       6

Контрпример вывода Z3

5 голосов
/ 02 февраля 2012

Когда формула в Z3 является ненасыщенной и (get-proof) указана, есть вывод, который я не нахожу никакой информации о том, что это такое.Где я могу найти какую-либо документацию по этому поводу?

Мне кажется совершенно нечитабельным, есть ли какой-нибудь инструмент, который принимает это в качестве ввода?

Cheers, Matt

1 Ответ

7 голосов
/ 02 февраля 2012

«Доказательства» Z3 не предназначены для потребления человеком.Устаревшая версия формата описана в документе: Доказательства и опровержения и Z3 .Файл z3_api.h содержит подробное описание каждого из правил проверки.Идентификаторы правила проверки начинаются с Z3_OP_PR.Мне известны два приложения, которые используют объекты доказательства Z3.Следующие документы содержат много примеров и описывают, как можно использовать объекты доказательства.

  1. Интерактивное доказательство теорем Изабель: доказательства Z3 восстанавливаются внутри Изабель с использованием доверенного ядра.Вы можете найти несколько статей, описывающих эту работу и формат доказательства Z3, на на домашней странице Саши Бома

  2. Генерация интерполантов

    Как сказал pad, unsat-cores гораздо проще в использовании.

...