

There are currently two prototype implementations of Linc.
The first, called BLinc, is an interactive theorem prover, built using
lambdaprolog with a Java interface. The second, the Level 0/1 prover, is an
automated prover, implemented using SML/NJ.
Level 0/1 Prover
 Download.
 Binaries: Here is the binary file for
Linux (x386 architecture) and here is the
binary file for Windows. (in
compressed zipformat).
 Source codes for
version 1.0.
Parts of the codes make use of the higherorder pattern unification
algorithm by Gopalan Nadathur and Natalie Linnel. The source codes for
the higherorder pattern unification can be downloaded
here.

 System requirements. You must have SML NJ version 110.46 or
later version installed. Standard ML can be obtained from
http://www.smlnj.org. 
 Running the prover. Download the binary file suitable for your
system, uncompress it, you'll get a file named 'level01'. Then run sml
with the following parameter: 
sml @SMLload=level01
 Documentation. A tutorial introduction is available
here.
An updated version of this tutorial, which includes overview of the logic behind the prover,
can be found in this paper. Some examples are included in
the source distribution source distribution, which includes,
among others, picalculus, bisimulation and modal logics. 
