Proving a graph well founded using resolution
Bezem, Jan Friso Groote · Logic Group preprint series · 1994
Using the resolution theorem prover OTTER we prove that a certain directed graph has no infinite path. We argue that this technique complements the well known combinatorial algorithms in cases in which the graph has a symbolic definition and a very large (or infinite) vertex set. The graph arose in the verification of a communication protocol.