The Madison Proof-Checking Language
madison
Version: 0.1
Revision : 2011.1202
Download
Latest: | madison-0.1-2011.1202.zip |
Requirements
- To test: Falderal
Description
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.
Documentation
- Madison.falderal (generated from doc/Madison.falderal)
Browse
- doc/
![[Valid XHTML 1.0]](../../images/buttons/valid-xhtml10.png){kind=small}