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.