Interactive prover for Multiplicative Linear Logic
by Ozan Kahramanogullari - ozan.kah@gmail.com

The tool implements the deep inference system MLSdli.

There is support for exporting to LaTeX.

To run double-click on the executable file or run it from command line.

Example input structures:
-------------------------

[  1 | 1  | 1 | ( bot * bot * bot ) ]

[  ( a * b ) | ( a * b )  | ( [ -a | -b ]  * [ -a | -b ] ) ]

[ -a |  -b | ( a *  b * [ -c | -d | ( c * d )  ]  )  ]

[  a | b  | c  | ( -a  *  -b  * -c )  ]

[ -a |  -b | ( a  *  b  * [ -c  | -d  | ( c * d * [ -e  | -f  | ( e * f ) ] ) ] ) ]

[ -a |  -b | ( a * b * [ -c  |  -d  |  ( c  *  d  * [ -a  |  -b  | ( a * b ) ] ) ] ) ]

[ -a | -b | ( a *  b * [ -a |  -b | ( a  *  b  * [ -a |  -b | ( a * b ) ] ) ] ) ] 

[  -c | ( -d  * - e )  |  ( e * -a )  | ( c * [ a | d ] )  ]
