Provides a function for calling external checkers using a Unix command.

Incremental verification of local confluence

Checking that a rule preserves typing (subject reduction property).

Representation of trees as graphviz files.