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

1 Introduction

Twelf is the current version of a succession of implementations of the logical framework LF. Previous systems include Elf (which provided type reconstruction and the operational semantics reimplemented in Twelf) and MLF (which implemented module-level constructs loosely based on the signatures and functors of ML still missing from Twelf).

Twelf should be understood as research software. This means comments, suggestions, and bug reports are extremely welcome, but there are no guarantees regarding response times. The same remark applies to these notes which constitute the only documentation on the present Twelf implementation.

For current information including download instructions, publications, and mailing list, see the Twelf home page at http://www.cs.cmu.edu/~twelf/. This User's Guide is published as

 Frank Pfenning and Carsten Schuermann
 Twelf User's Guide
 Technical Report CMU-CS-98-173, Department of Computer Science, 
 Carnegie Mellon University, November 1998.

Twelf Home Page

Below we state the typographic conventions in this manual.

code: for Twelf or ML code
`samp': for characters and small code fragments
metavar: for placeholders in code
keyboard: for input in verbatim examples
key: for keystrokes
math: for mathematical expressions
emph: for emphasized phrases

File names for examples given in this guide are relative to the main directory of the Twelf installation. For example `examples/guide/nd.elf' may be found in
`/usr/local/twelf/examples/guide/nd.elf' if Twelf was installed into the `/usr/local/' directory.

New Features: Differences from Twelf 1.2
Quick Start: Sample interaction with Twelf

1.1 New Features

The current version 1.3 from September 13, 2000 incorporates the following major changes from Twelf 1.2 from August 27, 1998.

Constraints (see section 6 Constraint Domains).: Type reconstruction and the logic programming engine (but not yet the theorem prover) allow various constraint domains in the style of constraint logic programming languages. The main ones are equalities and inequalities over rationals and integers.
Tracing and Breakpoints (see section 10.5 Tracing and Breakpoints): The logic programming engine now support tracing and setting of breakpoints for illustration and debugging purposes.
Theorem Prover (see section 9 Theorem Prover): The theorem prover now allows quantification over regular context. The theorem prover will also use previously proved theorems with %prove) and ignore those with %establish, which is otherwise equivalent. In unsafe mode, %assert can be used to claim theorems. However, at present no longer generates proof terms.
Reduction Checking (see section 8.2 Reduction Declaration): The termination checker has been extended to verify if output arguments to a predicate are smaller than some inputs with the %reduces declaration.
Signature Printing (see section 10.4 Signature Printing): Signatures can now be printed, also in TeX format.
Abbreviations (see section 3.3 Definitions): Added abbreviations (%abbrev) which, unlike definition, do not need to be strict.
Name Preferences (see section 3.5 Name Preferences): Name preference declarations (%name) now allow an optional second argument for naming of parameters.

1.2 Quick Start

Assuming you are running on a Unix system with SML of New Jersey already installed (see section 13 Installation) you can build Twelf as follows. Here `%' is assumed to be the shell prompt. You may need to edit the file `Makefile' to give the proper location for sml-cm.

% gunzip twelf-1-3.tar.gz
% tar -xf twelf-1-3.tar
% cd twelf
% make
% bin/twelf-server
Twelf 1.3, Sep 13 2000
%% OK %%

You can now load the examples used in this guide and pose an example query as shown below. The prompt from the Twelf top-level is `?-'. To drop from the Twelf top-level to the ML top-level, type C-c (CTRL c). To exit the Twelf server you may issue the quit command or type C-d (CTRL c).

Config.read examples/guide/sources.cfg
Config.load
top
?- of (lam [x] x) T.
Solving...
T = arrow T1 T1.
More? y
No more solutions
?- C-c
interrupt
%% OK %%
quit
%

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