A sequent calculus is proposed for machine-oriented proof search in intuitionistic first-order logic without equality. One of its distinctive features is that for optimizing quantifier handling, the author’s original notions of admissibility and compatibility of substitutions of terms for variables are used. Another is that the selection of some proportional rules for its application in an inference tree is “driven” by a formula from the succedent of a sequent under consideration. The proposed calculus is sound and complete and can serve as a basis for constructing provers for proof search in intuitionistic first-order logic.