A Linear Logic Prover (llprover). This small program searches a cut-free proof of the given two-sided sequent of first-order linear logic. Of course, the proof search of linear logic is undecidable. Therefore, this program limits the number of contraction rules for each path of the proof at most three (this threshold value can be changed). Formulas including additives, exponentials, or quantifiers can not be converted to Proof-net. To format LaTeX output, you need two style files: proof.sty (by Makoto Tatsuta) and linear.sty (does not work on LaTeX2e).

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element