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


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.