Downloads

		Downloads

08/24/04

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

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

BLinc

Download.

	The 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).
	Here are the source files, compressed using zip format.

System 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 http://java.sun.com.
	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 http://teyjus.cs.umn.edu/ .

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.

Compilation.

	To compile the lambda prolog source, type in: 'tjcc lincserver'.
	To compile the Java source code: 'javac *.java'.
	BLinc makes use of the following free softwares: lambdayacc parser generator and lexical analyzer for Java JFlex.

License information. BLinc is distributed under the GNU Public License. See this file for details.

Documentation. 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