Proof Net Calculator

Proof net calculator is a library of functions (or methods) for dealing with MLL proof nets of Linear Logic without the units. It has a proof search engine based on proof net construction, a normalization procedure based on Geometry of Interaction, a compiler for the linear lambda calculus into MLL proof nets, and translator to linear lambda terms in intuitionistic proof nets. Proof net calculator also has a simple GUI tool, which displays MLL proof nets on the PC screen and outputs encapsulated postscript files for them. Its implementation has been done using the programming language Scala, which is a functional extension of Java. Our implementation accommodates normalization and enumeration of relatively large numbers of proof nets.   

Download for sources

Instructions

How to Use

I suppose that you use the Microsoft windows system. But even if you use another system, then you can adapt these instructions to your system easily. I assume that your system already has installed JVM, Scala system, and simple build system. Otherwise, go to

http://java.com

and

http://www.scala-lang.org/download/

and

http://www.scala-sbt.org/

Download the proof net calculator package above.  I suppose that your directory is %HOME%. Then  make the ScalaProjects directory. Put the downloaded zip file in this directory and unzip it. Start your command prompt shell. Go to %HOME%\ScalaProjects\ProofNetCalculator. Then enter

    sbt

(for the first time, it will take a long time) and see ReadMe files in  %HOME%\ScalaProjects\ProofNetCalculator\Examples in order to know how to run  this software.

 

Principal Commands

Commands in the main object

When you 'run' in sbt, you should select no.1 to use the object.

The following are major commands:

Graphical User Interface

If you use graphical user interface, then when you 'run' in sbt, you should select no.2

How to Develop

You need to install java development kit (Jdk). Go to http://www.oracle.com/technetwork/java/javase/downloads/index.html

After installing jdk, you should set the environment variable JAVA_HOME to the directory which you have installed jdk (e.g., c:\Program Files (x86)\Java\jdk1.8.0_131).

The most preferable choice is to use Scala IDE (based on the eclipse). You can download this from

http://scala-ide.org/

Install Scala IDE following the instructions of the web site.

Then Start your command prompt shell. Go to %HOME%\ScalaProjects\ProofNetCalculator. Then enter

    sbt

In the sbt shell, enter

    eclipse .

Then the project file for Scala IDE is generated. After that, run Scala IDE (eclipse.exe). Then choose the workspace as %HOME%\ScalaProjects. Then you choose File->Import..->Existing Projects into Workspace and then ProofNetCalculator. Then you can find ProofNetCalculator package.