Let us say that we have 3 statements:
1. A>B
2. B>C
3.A
From here, a total of 3 conclusions can be reached: ____________________________________________________________________
4. B
5. C
6. A>C
It is clear that here, all the possible conclusions that could be derived, has been derived, and is also clear as to what the proof is for each derivation to the trained logician.
Howewer, given a more complex premise, say:
1. A+B
2. A=(C&D)
3. B>(D&G)
4. ~D+G
5. ~G
Whilst it may (or may not) be clear as to how one may go about deriving a single statement, it's not at all clear as to how one would go about deriving an exhaustive list of all statements.
I believe this is important because there may be one derivation that does not logically contradict another, but it does so via the context under which those derivations are being made (i.e the significance it bears on the real world). Or maybe they do not contradict each other, but they reinforce each other in such a way that can only be known by the agent constructing such a proof.
Now, of course with respects to logic itself, the context of the situation does not matter. However, the question as to "How can we know when all conclusions have been derived" is a question concerning pure logic, and because an answer to such a question does have real-world implications, I think it's a question worth asking.
Note: I do not include as part of the set of all derivations those that are logically true or false, for e.g A+B, A+(B&D), A&F, etc.
An exhaustive list of all formulas that can be derived is not finite, since there are infinitely many logical formulas that you could derive even without any assumptions. For example, you could always derive the tautologies $A\to A;$ $A\to(A\to A);$ $A\to(A\to(A\to A))$, etc.
So perhaps it is better to work with equivalence classes of formulas, since if $A$ and $B$ are equivalent to each other, then we can always use the proof of this equivalence to transform a proof of $A$ into a proof of $B$.
To be precise, instead of working with formulas $\phi$, we work with sets of formulas $[\phi]$, being the set of all formulas that are provably equivalent to $\phi$. We call such a set $[\phi]$ an equivalence class.
A formula $\psi$ is part of the equivalence class of $\phi$ if $\psi\leftrightarrow \phi$ is provable. For example, $B$ and $B\land B$ and $(A\lor\lnot A)\land B$ are all provably equivalent to each other, so they are all part of the same equivalence class.
This is probably what you meant with "vacuous".
Throughout the following I assume we're working with a finite set of premises, although it could be generalised to work with infinitely many premises.
Idea 1
Remember that a proof is nothing more than a finite list of formulas, such that each formula is either an axiom, a premise, or follows from an earlier formula in the list by the use of a derivation rule.
The precise specifics of what these axioms and derivation rules are, depends on the proof system you use, but the following idea works similarly for any proof system with a finite number of axioms and derivation rules. For example, you could use a Hilbert system for propositional logic. On that link there is an example of one with four axioms and a single derivation rule (modus ponens).
We can then define the length of a proof as the length of the list of formulas that make up the proof.
Generating the set of derivable formulas from a given set of premises is now quite "easy":
Since there are only finitely many derivation rules and axioms in a reasonable proof system for propositional logic, there are only a finite number of proofs of a given length $n$, so this process is possible, although it is an infinite process.
If you skip writing down formulas in your list that are logically equivalent to an earlier formula, you will get a list of formulas that are all unique with regard to logical equivalence. If you start with finitely many premises, there will be finitely many formulas in your list.
One problem with this approach is that we don't know if we have found all equivalence classes that are derivable: we don't know if we can stop at a given moment, or if we will still find new formulas if we keep going.
Idea 2
Another way would be to use semantics (so for propositional logic, this means truth tables) and the fact that propositional logic is complete: if we can prove an implication using truth tables, then we can find a derivation for it in our proof system (e.g. the Hilbert system I mentioned before).
There are at most $2^{2^m}$ equivalence classes of formulas using $m$ propositional variables. You can prove this by looking at truth tables: the equivalence class to which a formula belongs is decided by which rows of the truth table make it valid. If two formulas are valid on exactly the same rows, then those two formulas are equivalent to each other.
There are $2^m$ rows, hence $2^{2^m}$ possible combinations of these rows, each giving an equivalence class.
As an example, take the propositional variables $p_1,\dots,p_m$, and define for each subset $A\subseteq\{1,2,\dots,m\}$ the formula
$$\varphi_{A}=\left(\bigwedge_{i\in A}p_i\right)\land\left(\bigwedge_{i\notin A}\lnot p_i\right)$$
Each of these formulas is essentially a row in the truth table.
Then taking disjunctions of such formulas $\phi_A$ give you formulas for each equivalence class, since the disjunctions in a way "add" different rows together.
(Note that an empty conjunction is considered vacuously true $\bigwedge_{i\in \emptyset}p_i = \top$, and an empty disjunction is considered vacuously false $\bigvee_{i\in\emptyset}p_i = \bot$)
So, if we have a finite number $m$ of propositional atoms in our premises, we could simply make a list of $2^{2^m}$ formulas that are not equivalent to each other, and see for each of the formulas if it is implied by the premises. The resulting list gives us a set of formulas that are valid when the premises are valid.
By the completeness theorem, there is then a derivation for such formulas, and thus these formulas give us the equivalence classes we were after.