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 and simple build system (sbt). Otherwise, go to

and

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:

- run -checkLinearCC "file": check whether or not a given MLL proof structure (with one propositional variable) is an MLL proof net using a new linear time correctness condition described by

https://arxiv.org/abs/1902.09693

- run -checkLinearCC-WithHistory "file": generate a sequentialization list from a given MLL proof net (with one propositional variable) by a new linear time sequentialization algorithm by the author
- run -check "file": check whether or not a given MLL proof structure (with one propositional variable) is an MLL proof net using Girard's original definition of sequentialization (see also Examples\ProofStructures)
- run -checkDR "file": check whether or not a given MLL proof structure (with one propositional variable) is an MLL proof net using Danos-Regnier criterion (see also Examples\ProofStructures)
- run -checkDeNM "file": check whether or not a given MLL proof structure (with one propositional variable) is an MLL proof net using de Naurois-Mogbil criterion (see also Examples\ProofStructures)
- run -translate "file": transform MLL proof nets (with one propositional variable) that can be interpreted intuitionistically into linear lambda terms using Girard's original definition of sequentialization (see also Examples\IntuitionisticProofNets)
- run -linearML "file": transform linear lambda terms into MLL proof nets (with one propositional variable) (see also Examples\LinearLambdaTerms)
- run -IMLLFormula "file": transform IMLL formulas into MLL proof forests (with multiple propositional variables) (see also Examples\IMLLFormulas)
- run -cutElim "file": transform MLL proof nets (with one propositional variable) into MLL proof nets without cut-links using Girard's Geometry of Interaction (see also Examples\ProofStructures\CutElimination)
- run -constructMultiVarsByBT "file": when a given MLL proof forest with multiple propositional variables, enumerate all MLL proof nets for the forest (see also Examples\ProofForests)
- run -getOneConclusionPS "file": transform MLL proof structures with multiple propositional variables into those with single variable
- run -getOneConclusionForest "file": transform MLL proof forests with multiple propositional variables into those with single variable
- run -solveHCByBTDR "file": solve the Directed Hamiltonian Circuit problem (see also Examples\NPProblems\HamiltonianCircuits)
- run -solve3DMByBTDR "file": solve the 3D Matching problem (see also Examples\NPProblems\3DMatching)

**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_201).

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 "Welcome to IntelliJ IDEA" window, and then choose

"configures" -> "Plugins";

4. You see "Plugins" window and choose "Scala" and install it;

5. After the installation, choose “Restart IDE”;

6. Again you see "Welcome to IntelliJ IDEA" window, and then choose "Import Project"

and select "build.sbt” in the ProofNetCalculator package.