Immerman–Szelepcsényi 定理

非确定性天然适合证明“存在路径”，而补问题“没有路径”似乎需要记住整个可达集合。定理的突破是给分层可达集合计数，并让错误计数无法产生接受分支；通过逐层验证精确数量，可把全称式的不可达声明改造成可逐项核验的非确定性证书，在极小空间内证实不可达。它表明空间受限非确定性对补运算比时间受限情形更对称。

有向 $s$–$t$ 不可达性因此属于 NL，尽管直接交换可达性算法的接受、拒绝状态并不正确。定理证明的是空间类的补闭包，不推出 $\mathrm{L}=\mathrm{NL}$，也没有对应的已知结论 $\mathrm{NP}=\mathrm{coNP}$。

对有向图，设 $R_i$ 是从 $s$ 在至多 $i$ 步内可达的顶点集合。算法从 $|R_0|=1$ 开始，非确定地枚举并核验每个顶点是否从某个 $R_{i-1}$ 顶点一步到达，从而得到正确的 $|R_i|$；最终检查 $t\notin R_{n-1}$。

简单地“猜 $t$ 不可达”没有可验证内容，枚举某些路径也不能证明没有遗漏。定理需要 $s(n)\ge \log n$ 以保存顶点索引和计数，并推广为 $NSPACE(s(n))=coNSPACE(s(n))$，不只是一条 NL 特例。

NL 完全问题的补问题仍是 NL 完全问题；在低空间归约下，可达性与不可达性可以在同一复杂度类内相互使用。该定理也补齐了 Savitch 定理只给出确定性平方空间模拟、未给出同空间补闭包的一侧。

它直接给出 非确定对数空间类公理库复杂度类 NLComplexity class NL · Nondeterministic logspace可在非确定性对数空间内判定的语言类。 的补封闭性，即 $\mathrm{NL}=\mathrm{coNL}$，并以 STCON公理库STCON 的 NL 完全性NL-completeness of STCON · Directed reachability is NL-complete有向图可达性在确定性对数空间多一归约下是 NL 完全问题。 的补问题为核心。与 Savitch 定理公理库Savitch 定理Savitch's theorem对适当空间函数 s，NSPACE(s) 包含于 DSPACE(s²)。 的确定化上界不同，这里保留非确定空间而完成补封闭；它也说明 非确定空间类公理库非确定性空间复杂性类Nondeterministic space class · NSPACE由非确定性图灵机在给定空间界内判定的语言集合。 的结构不能照搬 NP 与 coNP 的直觉。