- Maude XEmacs Mode
You are a Maude and XEmacs user? You need it. - Coinductive Experiments in Maude
Some Maude modules specifying free categories with structure in order to do proofs by coinduction. Some simple facts about streams are proven this way. - Rational
Model Generator
Implementation in Prolog of a Tp operator for logic programs with negation. Generates "rational models". It's a reliable method for producing stack overflows.