Slothrop is an automated equational theorem prover that performs a variant of Knuth-Bendix completion. Instead of requiring an a priori term ordering to ensure convergence of rewriting, the space of orderings is searched. A termination checker is used to restrict search to the well-orderings. Input is given in TPTP format. A detailed description is available.
Based on an implementation of completion by Franz Baader and Tobias Nipkow, copyright 1998 Cambridge University Press, and on supporting data structures copyright 2003 Jean-Christophe Filliatre.
Contact Ian Wehrman for more information.