But is a Hilbert system easier to run in a computer since there are many axioms which clarifies the cases where contradictions or some inference rules are used

But is a Hilbert system easier to run in a computer since there are many axioms which clarifies the cases where contradictions or some inference rules are used which might be hard to program? For example, on the top of my head, in predicate logic, how would you encode an inference rule like exists elimination? It's tricky enough for me to think about, but to be able to encode a computer with it, is harder, and I can't remember if something like this falls under the undecidable problems category or not.