  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.
