命題の依存グラフ

条件 (U) を満たす文書の集合 $K$ について、環境の全体を $N$ とし、次のように分ける。

• $B \subseteq N$：基礎。定義と公理（証明を要しないと決めた種類の環境）。
• $S = N \setminus B$：定理類。そのうち証明をもつものの全体を $P \subseteq S$ とする。

$s \in P$ に対し、証明の中の参照のうち解決できたものが指す環境の集合を

（$d$ は $s$ のある文書）とし、$s$ の前提と呼ぶ。有向グラフ $G_K = (N, E)$、$E = \{(u, s) : s \in P,\ u \in \mathrm{prem}(s)\}$ を命題の依存グラフという。辺 $(u, s)$ は「$s$ の証明が $u$ を使う」ことを表す。