Philipp Rümmer, Hossein Hojjat and Viktor Kuncakプログラム検証の文脈で使われている Craig interpolation の変種たちを CHC solving を使って分類した論文（計算量などの性質についても少し議論されている）技術的な結果としては各種 interpolation と各…