Proof Net Calculator

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.

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

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.

Principal 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 -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_131).

The most preferable choice is to use Scala IDE (based on the eclipse). You can download this from

http://scala-ide.org/

Install Scala IDE following the instructions of the web site.

Then Start your command prompt shell. Go to %HOME%\ScalaProjects\ProofNetCalculator. Then enter

sbt

In the sbt shell, enter

eclipse .

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.