[ << ] [ < ] [ Up ] [ > ] [ >> ]         [Top] [Contents] [Index] [ ? ]

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.


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated on July 9, 2016 using texi2html 5.0.