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

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.

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