Поддерживает ли Z3 интерполяцию Крейга?

Может ли Z3 генерировать интерполянты Крейга (по крайней мере, для пропозициональной логики?). Я не нашел его в документации Z3.


z3
person Andreas Morgenstern    schedule 10.08.2011    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Нет, Z3 не поддерживает интерполянты Крейга, но генерирует пруфы. Интерполянты могут быть извлечены из доказательств. Кен Макмиллан разрабатывает генератор интерполяций поверх Z3, используя этот подход.

person Leonardo de Moura    schedule 10.08.2011
comment
Спасибо за ответ. Вы знаете о статусе проекта? Будет ли она закончена через пару дней, недель, месяцев? - person Andreas Morgenstern; 11.08.2011
comment
Интерполирующая процедура решения Кена уже используется. В конечном итоге он сделает его доступным на веб-сайте MSR. Пока он выпускает его в индивидуальном порядке. Вы можете связаться с ним, чтобы получить его процедуры. - person Leonardo de Moura; 11.08.2011