interana: interactive prover for Multiplicative Linear Logic

    There is support for exporting to LaTeX.
   
    download

     
     The tool implements the deep inference system MLSdli, defined in the following paper.     

     Interaction and depth against nondeterminism in proof search. [LINK]  

      Ozan Kahramanoğulları,

     

Logical Methods in Computer Science,

 

10 (2:5),

 

2014.