We present a complete proof synthesis method for the eight type systems of Barendregt's cube extended with $\eta$-conversion. Because these systems verify the proofs-as-objects paradigm, the proof synthesis method is a one level process merging unification and resolution. Then we present a variant of this method, which is incomplete but much more efficient. At last we show how to turn this algorithm into a unification algorithm.

翻译：我们提出了一种针对Barendregt立方体中八种类型系统（扩展了$\eta$-转换）的完全证明合成方法。由于这些系统验证了"证明即对象"范式，该证明合成方法是一个将合一与消解合并的单层过程。随后我们提出该方法的变体，它虽不完全但效率更高。最后，我们展示了如何将该算法转化为一个合一算法。