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.

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

and

http://www.scala-lang.org/download/

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**

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

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

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.