Existence of simple paths in ACL2
Nathan Wetzler
October 6, 2011


Graphs play a key role in many algorithms and systems.  Unfortunately,
support for graph theory in automated reasoning systems tends to be
inadequate or even nonexistent.  Ultimately, our goal is to develop a
system that allows users to mechanize reasoning about graphs while
still being able to work at a higher level of abstraction--one that
might be used on a blackboard, for example.  The first such step that
we have taken towards reaching this goal has been to construct a proof
of correctness for Prim's algorithm in ACL2, an interactive theorem
prover.

By mechanically verifying graph-based algorithms, such as Prim's, we
establish libraries that can be used towards the verification of
other, possibly larger, graph-based algorithms.  Such a library would
contain a theorem about the existence of simple paths in a graph.  In
this talk, we will present a proof for this theorem, examine where the
theorem fits into a larger proof about Prim's algorithm, and briefly
discuss why formally reasoning about graph theory is difficult.