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.