Jakie algorytmy są znane z obliczania interpolantów Craiga?

Czy istnieje przegląd algorytmów obliczania interpolantów? Co z artykułami na temat tylko jednego algorytmu? Najbardziej interesuje mnie przypadek i C = q plus ograniczenie, że interpolant jest tak mały, jak to możliwe. (Znam pracę McMillana z 2005 roku , która opisuje, jak uzyskać interpolanty, unikając kwantyfikatorów.)$A=\lnot p\land q$$C=q$

Tło: Interpolacja Craiga tw (1957) stwierdza, że jeśli , gdzie oznacza ( fol ) Wzór w T, A i C, to wzór T C , to jest wzór B tak, że ⊢ T → B i ⊢ T C B → C . Wzór B jest Craig interpolant z i$\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$(lub, w alternatywnych definicjach, i ¬ C ). Trywialnym interpolantem ¬ p ∧ q i q jest q , ale chcę małego interpolanta, dla pewnej rozsądnej definicji „małego” (takiego jak rozmiar składniowy). (Interpolanty mają wiele zastosowań, a jeśli jesteś ciekawy, oto jeden .)$A$$\lnot C$$\lnot p\land q$$q$$q$

Motywacja: Byłoby to przydatne w (bardzo) przyrostowej weryfikacji programu poprzez generowanie warunków weryfikacji.

Spójrz na rozprawę doktorską Himanshu Jaina , Weryfikację za pomocą sprawdzania satysfakcji, orzeczenie abstrakcji i interpolację Craiga . Rozważa wykonanie kilku podstawowych technik pod kątem zastosowań w weryfikacji, i ma rozdział dotyczący interpolacji wzorów obejmujących równania liniowe i diofantyny.

W szczególny sposób przygląda się metodzie połączenia Bibela, którą nazywa General Matings. Są to podejścia oparte na grafach, a nie oparte na formułowaniu podejścia do satysfakcji. Jeśli jesteś nimi ogólnie zainteresowany, pozwól mi polecić dość krótkie Dowody Dominika Hughesa (11 stron) bez składni .

Co ciekawe, istnieje związek między eliminacją cięć a twierdzeniem o interpolacji. Przede wszystkim twierdzenie o interpolacji wygląda jak odwrotność eliminacji reguły mieszania stosowanej podczas eliminacji cięcia. Ta eliminacja mówi:

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

Teraz jedną formę twierdzenia o interpolacji opartą na próbach bez cięć można wykonać w następujący sposób. To odwrócona wersja eliminacji. Zaczyna się od G, D | - B i daje G | - A i 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

Celowo stawiam średnik między przesłankami G i D. W tym miejscu wyznaczamy linię, które przesłanki chcemy widzieć jako dostarczające interpolant, i które założenia chcemy widzieć przy użyciu interpolantu.

Gdy dane wejściowe są próbą bez cięć, wysiłek algorytmu jest proporcjonalny do liczby węzłów próby bez cięć. Jest to więc praktyczna metoda liniowa na wejściu. Z każdym krokiem proof of cut-proof algorytm składa interpolant, wprowadzając nowy element łączący.

Powyższe spostrzeżenie dotyczy prostej konstrukcji interpolacji, w której wymagamy jedynie, aby interpolant miał jednocześnie propozycje z G i D. Interpolanty ze zmiennym warunkiem wymagają nieco więcej kroków, ponieważ trzeba również wykonać pewne blokowanie zmiennej.

Prawdopodobnie istnieje związek między minimalną odpornością na przecięcie a rozmiarem interpolantu. Nie wszystkie odcięcia próbne są minimalne. Na przykład jednolite proofy są często krótsze niż proofy bez cięć. Lemat dla jednolitych dowodów jest dość prosty, zastosowanie reguły w formie:

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

Można tego uniknąć, gdy B nie jest użyte w dowodzie C. Gdy B nie jest użyte w dowodzie C, mamy już G | - C, a przez to osłabienie G, A -> B | - C. Interpolacja algorytm wspomniany tutaj nie zwróci na to uwagi.

Z poważaniem

Odniesienia: Twierdzenie Craiga o interpolacji sformalizowane i zmechanizowane w Isabelle / HOL, Tom Ridge, University of Cambridge, 12 lipca 2006 Http://arxiv.org/abs/cs/0607058v1

Powyższa poprawność nie pokazuje dokładnie tej samej interpolacji, ponieważ używa wielu zestawów w końcowej części sekwencji. Nie wykorzystuje też implikacji. Ale to interesujące, ponieważ popiera moje twierdzenie o złożoności i ponieważ pokazuje zmechanizowaną weryfikację.

Minęły ponad dwa lata od momentu zadania tego pytania, ale w tym czasie opublikowano więcej artykułów na temat algorytmów obliczania interpolantów Craiga. Jest to bardzo aktywny obszar badawczy i nie jest możliwe podanie tutaj wyczerpującej listy. Wybrałem artykuły raczej arbitralnie poniżej. Proponuję następujące artykuły, które się do nich odwołują, i przeczytanie powiązanych rozdziałów pracy, aby uzyskać wyraźny obraz krajobrazu.

1. Skuteczne generowanie interpolacji w teorii satysfakcji Modulo , Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani, ACM TOCL, 2010.

   Obejmuje interpolację dla liniowej racjonalnej arytmetyki, racjonalnej i logicznej różnicy logicznej oraz logiki dwóch zmiennych na nierówność (UTVPI).

2. Efektywne generowanie interpolacji w zakresie satysfakcji Arytmetyka liczb całkowitych modulo , Alberto Griggio, Thi Thieu Hoa Le i Roberto Sebastiani. 2010 r.

3. Metoda kombinacji do generowania interpolantów , Greta Yorsh i Madanlal Musuvathi. 2005.

   Pokazuje, jak generować interpolanty w obecności kombinacji teorii Nelsona-Oppena.

4. Podstawowa interpolacja dla teorii równości , Alexander Fuchs, Amit Goel, Jim Grundy, Sava Krstic, Cesare Tinelli. 2011 r.

5. Kompletna interpolacja oparta na instancjach , Nishant Totla i Thomas Wies. 2012.

6. Interpolanty jako klasyfikatory , Rahul Sharma, Aditya V. Nori i Alex Aiken, 2012.