Complexity class of conditional dependency resolution

Question

I have a problem I am (considering) writing an algorithm for, but which I suspect to be NP-hard. However, I have not been able to prove that it is in fact NP-hard. The problem is stated as so:

Given a set of theorems, and a set of proofs for each of these theorems which may themselves depend on other theorems, find a list of proofs such that each proof only uses theorems which have proofs that precede it in the list.

The fact that these are theorems and proofs is immaterial as far as this problem is concerned; proofs can be considered to be mere sets of required theorems.

Answer 1

This seems to be solvable in quadratic time using the following algorithm (denote the number of theorems by $n$):

Let $L$ be an empty list.

While ( size of $L$ $<$ $n$):

• If there's a theorem provable by the theorems in $L$ (arbitrarily chose one if there are multiple such theorems), append the theorem to $L$.
• Else: return that no such ordering exist.

It's easy to see that if there exists some legal list of proving order, the algorithm will find such list.

Overall, we might need to go over all (remaining) theorems in each iteration, so the runtime is quadratic in the input size.