[ << ] | [ < ] | [ Up ] | [ > ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
The current version 1.4 from December 27, 2002 incorporates the following major changes from Twelf 1.3 from September 13, 2000.
World checking verifies regularity of the parameters and hypothesis
that can be introduced by terms in a signature. The new declarations
are %block
and %worlds
. This formally checks part of the
adequacy theorem that is usually left implicit in the encoding and is is
used centrally by the coverage checker.
Proofs of meta-theorems given in relational form can now be verified if
they are of order 2 or less. The new relevant declarations are
%covers
and %total
. The former can also be used to check
that sets of patterns in the arguments of a type family are exhaustive.
Mode checking has been extended so that multiple modes can be checked for the same predicate, even though not simultaneously. This allows certain relations to serve as proofs for biconditional meta-theorems. Also, some predicates in constraint domains can have multiple modes simultaneously in effect.
An experimental logic programming engine for tabled logic programming
is available in this release. The corresponding declarations
are %tabled a
(to declare a type family to be tabled)
and %querytabled
to start tabled search.
Type families can be declared deterministic for search, which means
that after the first solution has been found, backtracking will
not find any further solutions. The relevant declaration is
%deterministic a
.
Twelf now permits family-level definitions that are opaque to logic
programming execution. However, not all aspects of the present release
handle them properly, so they should be considered an experimental
feature. Furthermore, defined constants will now be used for
logic programming search when prefixed with %clause
.
Term reconstruction can print each typing judgment it establishes in order to help diagnose subtle type errors or ambiguities.
Twelf has been ported to be compliant with the Definition of Standard ML in its 1997 revision. As a result, it now supports Poly/ML and MLton in addition to Standard ML of New Jersey (SML/NJ).
[ << ] | [ < ] | [ Up ] | [ > ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
Assuming you are running on a Unix system with SML of New Jersey 110.0.3
already installed (see section 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
.
% gunzip twelf-1-4.tar.gz % tar -xf twelf-1-4.tar % cd twelf % make % bin/twelf-server Twelf 1.4, Dec 27 2002 %% OK %%
For SML/NJ version 110.20 or greater, use make -f smlnj/Makefile. For Poly/ML use make -f polyml/Makefile. For MLton use make -f mlton/Makefile.
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).
make examples/guide/sources.cfg top ?- of (lam [x] x) T. Solving... T = arrow T1 T1. More? y No more solutions ?- C-c interrupt %% OK %% quit %
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated on July 9, 2016 using texi2html 5.0.