Proof Net Calculator

 

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

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.

 

Major 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_162).

The most preferable choice is to use IntelliJ IDEA. You can download this from

https://www.jetbrains.com/idea/download/

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

Import Settings";

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

"SBT" plugins

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.