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[zip 3.8MB] for sources
- I suppose that you use the Microsoft windows system. But even if you use another operating system, then you can adapt these instructions to your system easily.
I assume that your system already has installed JRE and simple build system (sbt). Otherwise, go to
and/or
-
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.
- 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)