¿Qué algoritmos se conocen para calcular los interpolantes de Craig?

19

¿Hay alguna encuesta de algoritmos para calcular interpolantes? ¿Qué pasa con los documentos en un solo algoritmo? El caso que más me interesa es y , más la restricción de que el interpolante es lo más pequeño posible. (Conozco el artículo de McMillan de 2005 , que describe cómo obtener interpolantes, evitando los cuantificadores). $A=\lnot p\land q$ $C=q$

Antecedentes: el teorema de interpolación de Craig (1957) dice que si , donde es una fórmula ( fol ) en y es una fórmula de , entonces hay una fórmula tal que y . La fórmula es un interpolante de Craig de y (o, en definiciones alternativas, de y ). Un interpolante trivial de y es $\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$ , pero quiero un pequeño interpolante, para una definición razonable de 'pequeño' (como el tamaño sintáctico). (Los interpoladores tienen muchos usos y, en caso de que tenga curiosidad, aquí tiene uno ).

Motivación: Esto sería útil en la verificación (muy) incremental del programa mediante la generación de condiciones de verificación.

reference-request lo.logic proof-complexity feasible-interpolation Radu GRIGore
fuente

Hay varios resultados sobre la complejidad de encontrar el interpolante de una prueba dada en varios sistemas de prueba. En algunos sistemas de prueba débiles es posible encontrar el interpolante de manera eficiente (y luego decimos que el sistema de prueba satisface la propiedad de interpolación factible) pero los sistemas más fuertes no tienen esta propiedad asumiendo hipótesis plausibles en criptografía. Me resumen, el algoritmo para encontrar el interpolador depende del sistema de prueba se utiliza para lograr .

A \to C

$A \to C$

Kaveh

Debo estar perdiendo algo. El interpolante trivial

tiene tamaño 1. ¿Cómo puede ser más pequeño?

q

$q$

Emil Jeřábek apoya a Monica el

@ EmilJeřábek:

y

son una meta-variable, que significa fórmulas. Por ejemplo, podría tener

y

, en cuyo caso

es un buen interpolante de

p

$p$

q

$q$

p \equiv ((x = 1) \lor p r i m e (x))

$p\equiv((x=1)\lor{\it prime}(x))$

q \equiv ((x = 1) \land o d d (x))

$q\equiv((x=1)\land{\it odd}(x))$

f a l s e

${\bf false}$

\neg p \land q

$\lnot p\land q$ y

, porque

es insatisfactorio. En mi aplicación,

es una condición de verificación anterior , y

es la condición de verificación obtenida después de que el programa fue ligeramente editado.

q

$q$

\neg p \land q

$\lnot p\land q$

p

$p$

q

$q$

Radu GRIGore

Veo. Estoy bastante confundido por la notación. ¿Hay alguna razón por la cual

son minúsculas y

mayúsculas?

p, q

$p,q$

A, B, C

$A,B,C$

Emil Jeřábek apoya a Monica el

16

Eche un vistazo a la tesis doctoral de Himanshu Jain , Verificación mediante verificación de satisfacción, Predicación de abstracción e Interpolación de Craig . Considera el desempeño de varias técnicas fundamentales con vistas a las aplicaciones en la verificación, y tiene un capítulo sobre interpolación de fórmulas que involucran ecuaciones lineales y diofantinas.

Echa un vistazo particular a lo que yo conozco como el método de conexión de Bibel, y al que llama General Matings. Estos son enfoques de satisfacción basados en gráficos, en lugar de basados en la inferencia de fórmulas. Si está interesado en ellos en general, permítame recomendarle las pruebas razonablemente cortas (11 páginas) de Dominic Hughes sin sintaxis .

Charles Stewart
fuente

8

Curiosamente, existe una conexión entre la eliminación de corte y el teorema de interpolación. En primer lugar, el teorema de interpolación parece un reverso de la eliminación de la regla de mezcla utilizada durante la eliminación de corte. Esta eliminación dice:

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

Ahora, una forma de teorema de interpolación basada en pruebas sin cortes se puede hacer de la siguiente manera. Es la versión invertida de la eliminación. Comienza con G, D | - B y da G | - A y 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

Puse a propósito un punto y coma entre las premisas G y D. Aquí es donde dibujamos la línea, qué premisas queremos ver como entregando el interpolante, y qué premisas queremos ver usando el interpolante.

Cuando la entrada es una prueba sin cortes, el esfuerzo del algoritmo es proporcional al número de nodos de la prueba sin cortes. Por lo tanto, es un método práctico lineal en la entrada. Con cada paso de prueba de la prueba sin cortes, el algoritmo ensambla el interpolante al introducir un nuevo conector.

La observación anterior es válida para la construcción de interpolación simple, donde solo requerimos que el interpolante tenga proposiciones simultáneas de G y D. Los interpolantes con una condición variable requieren un poco más de pasos, ya que también es necesario realizar algunas variaciones variables.

Probablemente hay una conexión entre la minimidad de la prueba sin cortes y el tamaño del interpolante. No todas las pruebas sin cortes son mínimas. Por ejemplo, las pruebas uniformes suelen ser más cortas que las pruebas sin cortes. El lema para pruebas uniformes es bastante simple, una aplicación de la regla de la forma:

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

Puede evitarse cuando B no se usa en la prueba de C. Cuando B no se usa en la prueba de C, ya tenemos G | - C, y por lo tanto debilitando G, A -> B | - C. La interpolación algoritmo mencionado aquí, no prestará atención a esto.

Atentamente

Referencias: Teorema de interpolación de Craig formalizado y mecanizado en Isabelle / HOL, Tom Ridge, Universidad de Cambridge, 12 de julio de 2006 http://arxiv.org/abs/cs/0607058v1

La referencia anterior no muestra exactamente la misma interpolación, ya que utiliza conjuntos múltiples en la parte de conclusión de una secuencia. Tampoco hace uso de implicación. Pero es interesante ya que respalda mi reclamo de complejidad, y ya que muestra una verificación mecanizada.

fuente

Jan, puedes usar matemáticas de estilo LaTeX en teoría.

Kaveh

8

Han pasado más de dos años desde que se hizo esta pregunta, pero en ese tiempo, se han publicado más artículos sobre algoritmos para calcular los interpolantes de Craig. Esta es un área de investigación muy activa y no es factible dar una lista completa aquí. He elegido artículos bastante arbitrariamente a continuación. Sugeriría seguir los artículos que hacen referencia a ellos y leer sus secciones de trabajo relacionadas para obtener una imagen clara del paisaje.

Generación eficiente de interpoladores en la teoría del módulo de satisfacción , Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani, ACM TOCL, 2010.

Interpolación de cubiertas para lógica aritmética racional lineal, lógica de diferencia racional y entera, y lógica de unidad dos variables por desigualdad (UTVPI).
Generación eficiente de interpoladores en módulo de satisfacción Aritmética de enteros lineales , Alberto Griggio, Thi Thieu Hoa Le y Roberto Sebastiani. 2010
Un método de combinación para generar interpoladores , Greta Yorsh y Madanlal Musuvathi. 2005

Muestra cómo generar interpolantes en presencia de la combinación de la teoría de Nelson-Oppen.
Interpolación terrestre para la teoría de la igualdad , Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli. 2011
Interpolación basada en instanciación completa , Nishant Totla y Thomas Wies. 2012
Interpolantes como clasificadores , Rahul Sharma, Aditya V. Nori y Alex Aiken, 2012.

Vijay D
fuente

¿Qué algoritmos se conocen para calcular los interpolantes de Craig?

Respuestas: