We give a new proof of a theorem of Mints that the positive fragment of minimal predicate logic is decidable. The idea of the proof is to replace the eigenvariable condition of sequent calculus by an appropriate scoping mechanism. The algorithm given by this proof seems to be more practical than that given by the original proof. A naive implementation is given at the end of the paper. Another contribution is to show that this result extends to a large class of theories, including simple type theory (higherorder logic) and second-order propositional logic. We obtain this way a new proof of the decidability of the inhabitation problem for positive types in system F.

翻译：我们给出了明茨定理的一个新证明，即极小谓词逻辑的正片段是可判定的。该证明的核心思想是将相继演算中的特征变量条件替换为适当的辖域机制。由此证明给出的算法似乎比原证明中的算法更具实用性。文末给出了该算法的朴素实现。另一个贡献是表明该结果可推广至一大类理论，包括简单类型论（高阶逻辑）和二阶命题逻辑。通过这一方法，我们得到了系统F中正类型居留问题可判定性的一个新证明。