Какие алгоритмы известны для вычисления интерполантов Крейга?

Есть ли обзор алгоритмов вычисления интерполантов? Как насчет работ только по одному алгоритму? Случай я больше всего интересует = ¬ р ∧ д и С = д , а также ограничение , что интерполянт настолько мал , насколько это возможно. (Мне известна статья Макмиллана 2005 года , в которой описывается, как получать интерполанты, избегая при этом квантификаторов.)$A=\lnot p\land q$$C=q$

Фон: интерполяционная теорема Крейга (1957) говорит, что если , где A - ( fol ) формула в T A, а C - формула T C , то существует формула B такая, что ⊢ Т → B и ⊢ T C B → C . Формула B является интерполятором Крейга для A и $\vdash_{T_A\cup T_C}A\to C$$A$$T_A$$C$$T_C$$B$$\vdash_{T_A}A\to B$$\vdash_{T_C}B\to C$$B$$A$$C$(или, в альтернативных определений, из и ¬ С ). Простейшая интерполянт ¬ р ∧ д и д является д , но я хочу небольшой интерполянта, для некоторого разумного определения «малые» (например, синтаксического размера). (Интерполанты имеют много применений, и, если вам интересно, вот один .)$A$$\lnot C$$\lnot p\land q$$q$$q$

Мотивация: Это было бы полезно при (очень) инкрементальной верификации программы посредством генерации условий верификации.

Взгляните на кандидатскую диссертацию Химаншу Джайна , « Проверка с использованием проверки удовлетворенности», «Предикатная абстракция» и «Крейгская интерполяция» . Он рассматривает эффективность нескольких фундаментальных методов, ориентируясь на приложения в верификации, и имеет главу по интерполяции формул с участием линейных уравнений и диофантов.

Он особо рассматривает то, что я знаю как метод соединения Бибеля, и которое он называет Генеральным спариванием. Это основанные на графике, а не основанные на формулах подходы к удовлетворяемости. Если вы интересуетесь ими в целом, позвольте мне порекомендовать достаточно короткие (11 страниц) доказательства Доминика Хьюза без синтаксиса .

Интересно, что существует связь между отсечением и теоремой об интерполяции. Прежде всего, теорема об интерполяции выглядит как обратное исключению правила смешивания, используемому во время исключения среза. Это исключение говорит:

If G |- A and D, A |- B are cut-free proofs,  
then there is a cut-free proof G, D |- B

Теперь одну из форм теоремы об интерполяции, основанную на доказательствах без вырезов, можно сделать следующим образом. Это перевернутая версия ликвидации. Он начинается с G, D | - B и дает G | - A и D, A | - B:

If G; D |- B is a cut free proof,  
then there is a formula A (the interpolant) 
and cut free proofs G |- A and D, A |- B,  
and A uses only propositions simultaneously from G and D

Я специально поставил точку с запятой между предпосылками G и D. Именно здесь мы проводим черту, какие предпосылки мы хотим видеть как доставку интерполанта, и какие предпосылки мы хотим видеть, используя интерполант.

Когда вход является доказательством без среза, усилие алгоритма пропорционально количеству узлов доказательства без среза. Таким образом, его практический метод линейного ввода. На каждом шаге доказательства доказательства без выреза алгоритм собирает интерполант, вводя новую связку.

Вышеупомянутое наблюдение справедливо для простой интерполяционной конструкции, где нам требуется только, чтобы интерполант имел предложения одновременно из G и D. Интерполанты с переменным условием требуют немного больше шагов, поскольку также необходимо выполнить некоторую привязку переменной.

Вероятно, существует связь между минимальностью доказательства без вырезов и размером интерполанта. Не все доказательства без вырезов минимальны. Например, единообразные доказательства часто короче, чем доказательства без вырезов. Лемма для равномерных доказательств довольно проста, применение правила вида:

 G |- A       G, B |- C
 ----------------------
     G, A -> B |- C

Можно избежать, когда B не используется в доказательстве C. Когда B не используется в доказательстве C, мы уже имеем G | - C, и, таким образом, ослабляя G, A -> B | - C. Интерполяция Алгоритм, упомянутый здесь, не будет обращать на это внимание.

С уважением

Список литературы: Интерполяционная теорема Крейга, формализованная и механизированная в Изабель / HOL, Том Ридж, Кембриджский университет, 12 июля 2006 г. http://arxiv.org/abs/cs/0607058v1

Вышеприведенная ссылка не совсем показывает ту же интерполяцию, поскольку она использует множественные множества в заключительной части последовательности. Также это не использует смысл. Но это интересно, поскольку оно поддерживает мое утверждение о сложности и так как показывает механизированную проверку.

Прошло более двух лет с тех пор, как был задан этот вопрос, но за это время было опубликовано больше статей об алгоритмах вычисления интерполантов Крейга. Это очень активная область исследований, и здесь невозможно дать полный список. Я выбрал статьи довольно произвольно ниже. Я хотел бы предложить следующие статьи, которые ссылаются на них и читать соответствующие разделы работы, чтобы получить четкое представление о ландшафте.

1. Эффективная интерполяционная генерация в теории удовлетворенности по модулю , Алессандро Симатти, Альберто Гриджио, Роберто Себастьяни, ACM TOCL, 2010.

   Охватывает интерполяцию для линейной рациональной арифметики, логики рациональных и целочисленных разностей и логики переменных второго модуля на неравенство (UTVPI).

2. Эффективная интерполяционная генерация в выполнимости по модулю линейной целочисленной арифметики , Альберто Гриджио, Тхи Тьё Хоа Ле и Роберто Себастьяни. 2010.

3. Комбинированный метод получения интерполантов , Грета Йорш и Маданлала Мусувати. 2005.

   Показано, как генерировать интерполанты при наличии комбинации теории Нельсона-Оппена.

4. Основание интерполяции для теории равенства , Александр Фукс, Амит Гоэль, Джим Гранди, Сава Крстич, Чезаре Тинелли. 2011.

5. Полная интерполяция на основе инстанции, Нишант Тотла и Томас Вис. 2012.

6. Интерполанты как классификаторы , Рахул Шарма, Адитья В. Нори и Алекс Айкен, 2012.