Formal knowledge
Dependency graph
A graph that records which facts or declarations rely on which others.
Definition
Dependency graph
A dependency graph has declarations as nodes and uses directed edges to record reliance.
The graph supports impact analysis, axiom-footprint calculation, and selection of useful missing facts. Direction must remain clear: a dependency is used by a fact, while a dependent uses that fact.
01
Example
If theorem B uses theorem A, the graph records A as a dependency of B and B as a dependent of A.
02
Important distinction
A graph edge records formal or declared reliance, not every historical idea that influenced a proof.
After reading this article, you should be able to
- Define Dependency graph in the sense used on this site.
- Trace dependencies and dependents in a small theorem graph.