Art

The Abstract Rewrite Tool (Art) developed by Sebastian Stabinger as a bachelor project is a tool to analyze abstract rewrite systems (ARSs). You can read an ARS from a file or alternatively create such a system in the graphical user interface. By implementing appropriate graph algorithms, the tool can automatically check elements of ARSs for the properties WN, SN, UN, WCR and CR. Besides the fully automatic mode, the more playful game mode allows the user to fill out a property table herself. By providing explanations and corrections in the case of wrong guesses, the tool helps to better understand ARSs.

Got curious? You can download the thesis, sources, and jar or look at the readme.

Eve

Eve (Eve Verifies Equality) is a tool to check the validity of a conjecture s ≈ t against a set of axioms E. In case the conjecture can be shown valid, a proof of s ≈ t using the axioms E is provided.
Internally, Eve attempts to derive a complete system R equivalent to E using MKBtt. If such a system can be computed and the R-normal forms of s and t are equal, the obtained rewrite proof is transformed to an equational proof applying only axioms in E.

You may want to talk to Eve via the web interface.