15 Examples

We give here only a brief reference to the examples in the `examples/' subdirectory of the distribution. Each example comes in a separate subdirectory whose name is listed below.

`arith'

Associativity and commutative of unary addition.

`ccc'

Cartesian-closed categories (currently incomplete).

`church-rosser'

The Church-Rosser theorem for untyped lambda-calculus.

`compile'

Various compilers starting from Mini-ML.

`cut-elim'

Cut elimination for intuitionistic and classical logic.

`fol'

Simple theorems in first-order logic.

`guide'

Examples from Users' Guide.

`incll'

Logic programming in ordered logic.

`kolm'

Double-negation interpretation of classical in intuitionistic logic.

`lp'

Logic programming, uniform derivations.

`lp-horn'

Horn fragment of logic programming.

`mini-ml'

Mini-ML, type preservation and related theorems.

`polylam'

Polymorphic lambda-calculus.

`prop-calc'

Natural deduction and Hilbert propositional calculus

`units'

Mini-ML extended with units (currently incomplete).

In each directory or subdirectory you can find a file `sources.cfg' which defines the standard configuration, usually just the basic theory. The `test.cfg' which also defines an extended configuration with some test queries and theorems. Most examples also have a `README' file with a brief explanation and pointer to the literature.

Go to the first, previous, next, last section, table of contents.