Сборники трудов ИСП РАН


Интерполяция формул с кванторами в CSIsat на основе инстанцирования.

В.С. Мутилин., М.У. Мандрыкин.

Аннотация

В статье рассказывается о том, как на основе инструмента CSIsat реализована интерполяция Крейга для формул с кванторами, заданных в рамках комбинации теорий вещественной линейной арифметики и неинтерпретируемых функций. Предложен способ реализации интерполирования таких формул с помощью инстанцирования подкванторных выражений с использованием внешнего SMT-решателя CVC3. В статье описываются изменения, которые были внесены в интерполятор и решатель для реализации поддержки кванторной интерполяции. Также приводятся результаты тестирования модифицированного интерполятора как на задачах, полученных из набора SMTLIB, так и на специально сгенерированных для этих целей задачах.

Ключевые слова

интерполяция, интерполянт Крейга, кванторы, инстанцирование, решатель, аксиомы

Издание

Труды Института системного программирования РАН, том 22, 2012, стр. 327-348.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-22-18

Полный текст статьи в формате pdf Вернуться к содержанию тома