The proof net calculator is a library of functions (or methods) for manipulating MLL proof nets of Linear Logic without the multiplicative 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 a translator of linear lambda terms into intuitionistic proof nets. The proof net calculator also has a simple GUI tool, which displays an MLL proof net on a PC screen and outputs an encapsulated postscript file for it. Its implementation has been done using the programming language Scala, which is an object-oriented functional programming language over the Java Virtual Machine. It can also solve NP-complete problems with search space reduction using backtracking and dependency relations of ID-links. Compared to a solver without these mechanisms, it is able to solve instances with much larger sizes.
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_162).
The most preferable choice is to use IntelliJ IDEA. You can download this from
After installing IntelliJ IDEA, you can import Proof net calculator as follows:
1. Start the IntelliJ IDEA;
2.You see "Complete Installation" window, and then choose "Do not
3.You see "Customize IntelliJ IDEA" window, and then choose "Skip
Remaining and Set Defaults";
4. You see "Welcome to IntelliJ IDEA" window, and then choose
"configures" -> "Plugins";
5. You see "Plugins" window, and then choose "Browse repositories";
6. You see "Browse Repositories" window, and then choose "Scala" and
and then click "Close" button;
7. You see "Plugins" window again, and then click "OK" button;
8. Then choose "Restart";
9. Again you see "Welcome to IntelliJ IDEA" window, and then choose "Open"
and select "ProofNetCalculator" directory;
10. Then you see "Import Project from sbt" window, and then link "Project
JDK" with your JDK directory and click "OK" button.