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.

## Sample Program

```
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
```

## Computational Class

## Programming Paradigms

## Defined by

Specs on Spec distribution

## Documentation

- README.markdown
- didigm/didigm.markdown
- irishsea/README.markdown
- irishsea/doc/environment.markdown
- irishsea/doc/language.markdown
- irishsea/doc/model.markdown
- irishsea/doc/original-notes.markdown
- madison/Madison.markdown
- mdpn/mdpn.markdown
- oozlybub-and-murphy/oozlybub-and-murphy.markdown
- opus-2/opus-2.markdown
- sampo/Practical_Matters.markdown
- sartre/sartre.markdown
- star-w/star-w.markdown
- tamerlane/tamerlane.markdown
- turkey-bomb/turkey-bomb.markdown
- you-are-reading-the-name-of-this-esolang/you-are-reading-the-name-of-this-esolang.markdown

## Download

## Development

Github: catseye/Specs-on-Spec

Issue tracker: on github