Proving a graph well founded using resolution

Abstract

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.