# 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.

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

http://java.com

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:

• 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

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

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.