#z3 #isabelle #smt
#z3 #isabelle #smt
Вопрос:
Во время чтения расширения Sledgehammer с помощью решателей SMT я прочитал следующее:
В оригинальной архитектуре Sledgehammer доступные леммы были переписаны в нормальную форму предложения с использованием наивного применения законов распределения до того, как был вызван фильтр релевантности. Чтобы избежать клаузирования тысяч лемм при каждом вызове, предложения хранились в кэше. Эта конструкция была технически несовместима с методом smt (без учета кэша), и она уже была неудовлетворительной для ATPS, которые включают в себя пользовательские клаузификаторы полиномиального времени.
Мое понимание SMT до сих пор заключается в следующем: SMT не работают над предложениями. Вместо этого они пытаются построить модель для части проблемы, не содержащей кванторов. Поиск уточняется путем создания кванторов в соответствии с некоторым набором активных терминов. Таким образом, действительно, для решателей SMT не требуется клаузальная форма.
Мы переписали фильтр релевантности так, чтобы он работал с произвольными формулами HOL, пытаясь имитировать старое поведение. Чтобы имитировать штраф, связанный с функциями Skolem в коде на основе предложений, мы отслеживаем полярности и обнаруживаем кванторы, которые приводят к функциям Skolem.
Какой штраф связан с функциями Skolem? Я мог бы понять, что они не подходят для SMT, но здесь кажется, что они также плохи для ATPS…
Ответ №1:
Во-первых, решатели SMT работают над предложениями, и внутри определенно существует некоторая (не наивная) нормализация (например, минископирование). Но вам не нужно выполнять нормализацию перед вызовом решателя SMT (особенно, поскольку это будет более наивно и сгенерирует большее количество предложений).
В любом случае, раздел 6.6.7 объясняет, почему сколемизация была выполнена на стороне Isabelle. Подводя итог: невозможно ввести полиморфные константы в доказательство в Isabelle; следовательно, это должно быть сделано до начала доказательства.
Представляется вероятным, что при написании статьи отсутствие изменения фильтрации привело к снижению производительности и, следовательно, был добавлен штраф. Тем не менее, я попытался найти соответствующий код, имитирующий клаусификацию в Sledgehammer, поэтому я не верю, что это происходит больше.
Комментарии:
1. Из вашего высказывания я делаю вывод, что «функции Skolem» (спасибо, что объяснили, откуда они берутся) имеют ограничение в производительности Sledgehammer. Так получается, что они наказывали вспомогательные леммы, содержащие функции Skolem, при фильтрации релевантности?
2. Да, скорее всего. Хотя это зависит от точных параметров фильтрации (мы заменяем экзистенциальный квантор константой с несколькими параметрами).