Quels algorithmes sont connus pour calculer les interpolants de Craig?

19

Existe-t-il un aperçu des algorithmes de calcul des interpolants? Qu'en est-il des articles sur un seul algorithme? Le cas qui m'intéresse le plus est et , plus la contrainte que l'interpolant est aussi petit que possible. (Je connais l'article de McMillan de 2005 , qui décrit comment obtenir des interpolants, tout en évitant les quantificateurs.) $A=\lnot p\land q$ $C=q$

Contexte: le théorème d' interpolation de Craig (1957) dit que si , où est une formule ( fol ) dans et est une formule de , alors il existe une formule telle que et . La formule est un interpolant Craig de et $\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$ (ou, dans d'autres définitions, de et ). Un interpolant trivial de et est , mais je veux un petit interpolant, pour une définition raisonnable de «petit» (comme la taille syntaxique). (Les interpolants ont de nombreuses utilisations et, si vous êtes curieux, en voici un .) $A$ $\lnot C$ $\lnot p\land q$ $q$ $q$

Motivation: Cela serait utile dans la vérification de programme (très) incrémentielle via la génération de conditions de vérification.

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

Il existe différents résultats sur la complexité de trouver l'interpolant à partir d'une preuve donnée dans divers systèmes de preuve. Dans certains systèmes de preuve faibles, il est possible de trouver l'interpolant efficacement (et nous disons ensuite que le système de preuve satisfait la propriété d'interpolation faisable) mais les systèmes plus forts n'ont pas cette propriété en supposant des hypothèses plausibles en crypto. Je court, l'algorithme pour trouver le interpolée dépend du système de preuve utilisé pour montrer

.

A \to C

$A \to C$

Kaveh

J'ai dû louper quelque chose. L'interpolant trivial

a une taille 1. Comment peut-il être plus petit?

q

$q$

Emil Jeřábek soutient Monica

@ EmilJeřábek:

et

sont des méta-variables, qui représentent des formules. Par exemple, vous pourriez avoir

et

, auquel cas

est un bon interpolant 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$ et

, car

n'est pas satisfaisant. Dans mon application,

est une ancienne condition de vérification , et

est la condition de vérification obtenue après que le programme a été légèrement modifié.

q

$q$

\neg p \land q

$\lnot p\land q$

p

$p$

q

$q$

Radu GRIGore

Je vois. Je suis assez confus par la notation. Y a-t-il une raison pour laquelle

sont en minuscules et

majuscules?

p, q

$p,q$

A, B, C

$A,B,C$

Emil Jeřábek soutient Monica le

16

Jetez un oeil à la thèse de doctorat de Himanshu Jain , la vérification utilisant la vérification de la satisfaction, l'abstraction des prédicats et l'interpolation Craig . Il considère les performances de plusieurs techniques fondamentales en vue d'applications en vérification et a un chapitre sur l'interpolation de formules impliquant des équations linéaires et des diophantines.

Il jette un regard particulier sur ce que je connais comme la méthode de connexion de Bibel, et qu'il appelle General Matings. Il s'agit d'approches de satisfiabilité basées sur des graphiques plutôt que sur des inférences de formules. Si vous les intéressez en général, permettez-moi de vous recommander les épreuves de Dominic Hughes raisonnablement courtes (11 pages) sans syntaxe .

Charles Stewart
la source

8

Il est intéressant de noter qu'il existe un lien entre l'élimination des coupures et le théorème d'interpolation. Tout d'abord, le théorème d'interpolation ressemble à l'inverse de l'élimination des règles de mélange utilisée lors de l'élimination des coupures. Cette élimination dit:

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

Maintenant, une forme de théorème d'interpolation basée sur des preuves sans coupure peut être effectuée comme suit. C'est la version à l'envers de l'élimination. Il commence par G, D | - B et donne G | - A et 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

Je mets volontairement un point-virgule entre les prémisses G et D. C'est là que nous dessinons la ligne, quelles prémisses nous voulons voir comme délivrant l'interpolant, et quelles prémisses nous voulons voir en utilisant l'interpolant.

Lorsque l'entrée est une preuve sans coupure, l'effort de l'algorithme est proportionnel au nombre de nœuds de la preuve sans coupure. Donc c'est pratique une méthode linéaire en entrée. À chaque étape de preuve de la preuve sans coupure, l'algorithme assemble l'interpolant en introduisant un nouveau connecteur.

L'observation ci-dessus est valable pour la construction d'interpolation simple, où nous exigeons seulement que l'interpolant ait simultanément des propositions de G et D.Les interpolants avec une condition variable nécessitent un peu plus d'étapes, car il faut également effectuer un masquage variable.

Il existe probablement un lien entre la minimalité de l'épreuve sans coupure et la taille de l'interpolant. Toutes les épreuves sans coupure ne sont pas minimes. Par exemple, les épreuves uniformes sont souvent plus courtes que les épreuves sans coupure. Le lemme des preuves uniformes est assez simple, une application de règle de la forme:

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

Peut être évité, lorsque B n'est pas utilisé dans la preuve de C. Lorsque B n'est pas utilisé dans la preuve de C, nous avons déjà G | - C, et donc en affaiblissant G, A -> B | - C. L'interpolation algorithme mentionné ici, ne fera pas attention à ce sujet.

Meilleures salutations

Références: Théorème d'interpolation de Craig formalisé et mécanisé dans Isabelle / HOL, Tom Ridge, Université de Cambridge, 12 juillet 2006 http://arxiv.org/abs/cs/0607058v1

La référence ci-dessus ne montre pas exactement la même interpolation, car elle utilise plusieurs ensembles dans la partie conclusion d'un séquent. Il n'utilise pas non plus d'implication. Mais c'est intéressant car il supporte ma revendication de complexité, et puisqu'il montre une vérification mécanisée.

la source

Jan, vous pouvez utiliser les mathématiques de style LaTeX sur cstheory.

Kaveh

8

Cela fait plus de deux ans que cette question a été posée, mais à cette époque, d'autres articles ont été publiés sur les algorithmes de calcul des interpolants de Craig. Il s'agit d'un domaine de recherche très actif et il n'est pas possible de donner ici une liste complète. J'ai choisi des articles plutôt arbitrairement ci-dessous. Je suggérerais de suivre les articles qui les référencent et de lire leurs sections de travail connexes pour obtenir une image claire du paysage.

Génération interpolante efficace de la théorie de la module de satisfaction , Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani, ACM TOCL, 2010.

Couvre l'interpolation pour l'arithmétique rationnelle linéaire, la logique de différence rationnelle et entière et la logique de l'unité deux variables par inégalité (UTVPI).
Génération interpolante efficace de la satisfaction Modulo Linear Integer Arithmetic , Alberto Griggio, Thi Thieu Hoa Le et Roberto Sebastiani. 2010.
Une méthode de combinaison pour générer des interpolants , Greta Yorsh et Madanlal Musuvathi. 2005.

Montre comment générer des interpolants en présence d'une combinaison de théorie Nelson-Oppen.
Interpolation au sol pour la théorie de l'égalité , Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli. 2011.
Interpolation basée sur l'instanciation complète , Nishant Totla et Thomas Wies. 2012.
Interpolants as Classifiers , Rahul Sharma, Aditya V. Nori et Alex Aiken, 2012.

Vijay D
la source

Quels algorithmes sont connus pour calculer les interpolants de Craig?

Réponses: