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,...