非终止性分析

由于停机问题的不可判定性，非终止性分析一般和终止性分析共同使用，试图直接从否定的角度证明程序的非终止性。在nontermination analysis中，尝试找到nontermination argument/proof。

最常见的一种非终止性论据是recurrence set，其存在性和非终止性等价（此外有一种变体closed recurrence set + 下近似）。Geometric nontermination argument也是一种非终止论据的形式。

此外，有尝试用形式逻辑系统对终止性问题进行建模，并用推理系统来证明，如一系列基于resource logic的工作（没有细看）。以及基于错误逻辑的Non-termination Proving at Scale。