Expression deduction algorithm in propositional logic

Question

I need to find a way to deduce an expression in propositional logic.

The given expression $\alpha$ contains up to $3$ variables.

I need to find a list of hypotheses $\Gamma$ consisting only of variables such that $\Gamma\vdash\alpha$. If such a list is found then I need to find a proof that $\Gamma\vdash\alpha$.

In case such list doesn't exist I need to find a list $\Gamma'$ consisting only of negations of variables such that $\Gamma'\vdash\neg\alpha$. If such list $\Gamma'$ exists then I need to find a proof that $\Gamma'\vdash\neg\alpha$.

The $\Gamma$ and $\Gamma'$ lists should contain minimal amount of variables.

It is still possible that none of the described lists can be found.

The proof is the sequence of expressions that can be:

1. Axiom
2. Modus Ponens application
3. Hypothesis (element of list $\Gamma$ or $\Gamma'$)

Axioms are as follows:

1. $\varphi\to\psi\to\varphi$
2. $(\varphi\to\psi)\to(\varphi\to\psi\to\pi)\to(\varphi\to\pi)$
3. $\varphi\to\psi\to\varphi\land\psi$
4. $\varphi\land\psi\to\varphi$
5. $\varphi\land\psi\to\psi$
6. $\varphi\to\varphi\lor\psi$
7. $\psi\to\varphi\lor\psi$
8. $(\varphi\to\pi)\to(\psi\to\pi)\to(\varphi\lor\psi\to\pi)$
9. $(\varphi\to\psi)\to(\varphi\to\neg\psi)\to\neg\varphi$
10. $\neg\neg\varphi\to\varphi$

I think I can find out if it's possible to find $\Gamma$ or $\Gamma'$ lists and prove the corresponding facts. My way to do this is to evaluate the expressions using all possible combinations of truth values for variables. If $\alpha$ is always true then list $\Gamma$ may be empty. If $\alpha$ is always false then list $\Gamma'$ may be empty. Otherwise I will check the expressions $A\to\alpha$, $B\to\alpha$, ..., $A\to B\to\alpha$, etc. in the same way. $A$, $B$ are examples of variables. In case, for example, $A\to\alpha$ is always true, then the list $\Gamma$ may contain only variable $A$. I hope the logic is clear. It shouldn't take a long time since there can be only up to $3$ variables.

However, I'm not sure how to construct the proof. I need to do it programmatically so there should be some algorithm to do this. I attempted to use the deduction theorem (and the ideas of its proof) for this but I don't know how to apply it when the expression is not an implication but a conjunction, for example.