I think this boils down to a question about how redex executes judgment forms. Leaving aside modeless judgment forms (where redex will only check a derivation for you but won't ever make them up), redex is turning each judgment form into a (fancy) function from the inputs to sets of the outputs and, based on how that function goes, will build a derivation for you.
So, in the example in your message, think of `infer` as a function that consumes the first thing and produces the second thing, where the part below the bar is a kind of case/choice and the part above the bar are recursive calls. So, if we want to use that rule, we'll be given "C" and have to come up with "B". To make the recursive call to infer for the premise, we have to supply an "A" which will then give us a "B". And now we're stuck because we don't have that "B".
Of course, there are many other ways that one could think of turning judgment forms into something that is, at least in some sense, executable. Doing something like prolog is an obvious choice (although Redex is more expressive than the standard/original prolog so there are some tricks required) and Redex does indeed use a prolog-inspired solver when it is generating random derivations that satisfy a judgment form (see Burke Fetscher's dissertation). One might also try to turn it into a SMT query, but Redex doesn't currently do that (and there aren't any plans to do that). Perhaps there is another way too.
So, as to your specific question, the answer is "it depends". If you can formulate your judgment form in a way that respects the mode, then yes, you can use premises to constrain the sets of valid judgments. If not, you can't.
hth,
Robby