Suppose we have an algorithm which, given a set of axioms $A$ and a sentence $P$ can prove if $A \implies P$. Would such algorithm be able to prove any possible theorem implied by these axioms? Is Gödel's theorem on incompletness relevant here?
EDIT: Seems the question got a bit misunderstood. I'm only interested in getting answers (tautology/unprovable/contradiction) on some particular theorems (sentences) given by the input, not a list of all possible sentences (which would be infinite in size, unless we reject equivalent sentences). (I am a CS student and a newbie to predicate logic/general low-level math).
The problem is that your assumption is false, when $A$ is simply PA (due to Godel's incompleteness theorem) and so you can deduce everything. In particular, your hypothetical algorithm will both halt and not halt.
On the other hand, you don't need your hypothetical algorithm at all, if all you want is to list out all theorems provable from $A$. Simply go through all proofs in length-lexicographic order and check if it is correct, and output the proven theorem (if not already output before).
However, if you want you can consider an oracle (not an algorithm) that decides whether $A \vdash φ$ given any decider (deciding algorithm) for $A$ and sentence $φ$. Then you can ask the question of whether you can use the oracle to do things. For one, you can use it to solve the halting problem.