Madison is a language in which one can state proofs of properties of term-rewriting systems. Classical methods of automated reasoning, such as resolution, are not used; indeed, term-rewriting itself is used to check the proofs. Both direct proof and proof by induction are supported. Induction in a proof must be across a structure which has a well-founded inductive definition. Such structures can be thought of as types, although this is largely nominal; the traditional typelessness of term-rewiting systems is largely retained.
type tree is tree(leaf) -> true tree(branch(X,Y)) -> and(tree(X),tree(Y)) in let reflect(leaf) -> leaf reflect(branch(A,B)) -> branch(reflect(B),reflect(A)) in theorem forall X where tree(X) reflect(reflect(X)) ~> X proof case X = leaf reflect(reflect(leaf)) -> reflect(leaf) [by reflect.1] -> leaf [by reflect.1] case X = branch(S, T) reflect(reflect(branch(S, T))) -> reflect(branch(reflect(T),reflect(S))) [by reflect.2] -> branch(reflect(reflect(S)),reflect(reflect(T))) [by reflect.2] -> branch(S,reflect(reflect(T))) [by IH] -> branch(S,T) [by IH] qed
Specs on Spec distribution