Tools on Rewriting
-
Autograph is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autograph is an experimental tool written in Common Lisp for verifying properties of graphs of bounded clique-width. It is written in Steele Bank Common Lisp (SBCL). It uses the Autowrite library which provides the operations needed to create and manipulate automata. The following famous theorem connects the problem of verifying graph properties with term automata: Monadic second-order model checking is for tree-width [Courcelle (1990)] and clique-width [Courcelle, Makowski, Rotics (2001)]. Tree-width and clique-width are graph complexity measures based on graph decompositions. A decomposition produces a term representation of the graph. For a graph property expressed in monadic second order logic (MSO), the algorithm verifying the property takes the form of a term automaton which recognizes the terms denoting graphs satisfying the property.
Autograph is now part of TRAG ... git clone https://idurand@bitbucket.org/idurand/trag.git...