Can anyone help me assemble a list of the constructive proofs of Craig's Interpolation Theorem for classical first order logic? A constructive proof means that a method is provided for producing the actual interpolant.
Here's the theorem for reference, copied from Wikipedia. Note, this version of the theorem is for propositional logic:
If $\models \varphi \to \psi$ then there is a $\rho$ (the interpolant) such that $\models \varphi \to \rho$ and $\models \rho \to \psi$, where $atoms(\rho) \subseteq atoms(\varphi) \cap atoms(\psi)$. Here, $atoms(\varphi)$ is the set of propositional variables occurring in $\phi$, and $\models$ is the semantic entailment relation for propositional [sic] logic.