Proving properties of directed graphs: a problem set for automated theorem provers
Gerhard Schellhorn · OPen Access Repositorium der Universität Ulm (OPARU) (Ulm University) · 1998
This paper describes a problem set for automated theorem provers taken from a KIV case study on the implementation of depth-first search on graphs. The goal is to prove 54 consequences of the axioms specifying directed graphs.