There are currently two prototype implementations of Linc. The first, called BLinc, is an interactive theorem prover, built using lambda-prolog with a Java interface. The second, the Level 0/1 prover, is an automated prover, implemented using SML/NJ.

Level 0/1 Prover

  • Binaries: Here is the binary file for Linux (x386 architecture) and here is the binary file for Windows. (in compressed zip-format).
  • Source codes for version 1.0. Parts of the codes make use of the higher-order pattern unification algorithm by Gopalan Nadathur and Natalie Linnel. The source codes for the higher-order pattern unification can be downloaded here.
bulletSystem requirements. You must have SML NJ version 110.46 or later version installed. Standard ML can be obtained from
bulletRunning 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

bulletDocumentation. 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, pi-calculus, bisimulation and modal logics.



bulletThe binary (Java byte code) is available in JAR-file format. You need the following files: BLinc.jar (user interface) and lincserver.lp (the inference engine).
bulletHere are the source files, compressed using zip format.
bulletSystem requirements:

You must have the Sun Java runtime environment installed. The current version has been tested on Java version 1.4.2. The latest Java runtime environment can be found at


You must have the Teyjus implementation of Lambda Prolog installed. The PATH environment must be set so that you can run 'tjsim' from a shell (in Unix) or a command prompt (Windows). The Teyjus distribution is available at .


Installation. Put the file BLinc.jar and lincserver.lp in the same directory and type 'java -jar BLinc.jar' to run. Or if you're using windows manager, double-click on the BLinc.jar icon.

bulletTo compile the lambda prolog source, type in: 'tjcc lincserver'.
bulletTo compile the Java source code: 'javac *.java'.      
bulletBLinc makes use of the following free softwares: lambdayacc parser generator and lexical analyzer for Java JFlex.
bulletLicense information. BLinc is distributed under the GNU Public License. See this file for details.
bulletDocumentation. There is a tutorial available and a few examples. The derivation files in the examples are those with the extension .drv and the definition files have the extension .def.

Home | Publications | Downloads | People | Feedback

This site was last updated 07/22/05