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
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
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
(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.
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
Install Scala IDE following the instructions of the web site.
Then Start your command prompt shell. Go to %HOME%\ScalaProjects\ProofNetCalculator. Then enter
In the sbt shell, enter
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.