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 cliquewidth. 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 secondorder model checking is for treewidth [Courcelle (1990)] and cliquewidth [Courcelle, Makowski, Rotics (2001)]. Treewidth and cliquewidth 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...