Computing Premises from Consequence

We write ‘If A, then B‘ to mean that if A is true, then B must be true because B is a logical consequence of A i.e. it is impossible for A to be true but B to be false.

Let us consider one such statement:

‘If S₁ , then S₂‘ is true,
where S₁, S₂ are expressions.

Let it also be the case that :
‘If S_i , then S₂‘ is true, and let there be many such S_i. For all such S_i and S₁, assume they do not contradict each other, and indeed there is a finite deduction from all S_i and S₁ to S₂.

Now for a given S₂, I want to generate a finite conjunction of expressions which, so to speak, encodes necessary properties of the premises so that the conclusion (S₂ in this case) is the logical consequence of the premise (all such S_i). Ideally, this expression must take in some input, and yield some S_i, and with appropriate set of constraints, we should be able to generate all S_i. (For sufficiency, we may append some disjunction expressions as well if need be).

Is there a method to generate such an expression?