From Strong Amalgamability to Modularity of Quantifier-Free Interpolation http://arxiv.org/abs/1203.3730 : SMTで理論T1,T2のinterpolationアルゴリズムを組み合わせてT1∪T2のinterpolationアルゴリズムを作りたいという話で、結合した理論のinterpolationに関する既存の結果を色々と一般化。

quantifier-free interpolantion と sub-amalgamation property が対応するが、これは theory combination に関して閉じていない。より強い strong sub-amalgamation property を考えると、stably infinite で signature disjoint な理論の結合に関して閉じている。しかも、quantifier-free interpolation が成り立つTについて、T∪EUFでquantifier-free interpolationが成り立つのと、Tがstrong sub-amalgamation propertyを満たすのと同値という意味で本質的。

理論が strong sub-amalgamation property を満たすことを示すのは簡単ではないので、同値となる証明論的な性質として equality interpolating という性質を定義している。 これ定義は分かるのだけど、どうも直観的な意味が分からない……

実際に、T1,T2のinterpolationを使ってT1∪T2のinterpolationを行うアルゴリズムについては、非決定的な部分が多いので、これを実際に使うのは難しそうだけど、面白い。 interpolationの導出のための体系としてこういうのを考えるというのも知らなかったので面白かった。