A Linear Logic Prover

, par Naoyuki Tamura

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).

Note that :

  • Occur check is not included.
  • Do not use free variables, i.e. formulas like a(X) --> a(1)) are not allowed.

Any comments or suggestions are appreciated.

System names, notations, and examples are based on Troelstra’s text book :

--- Exporter la sélection au format

Voir en ligne : The original linear logic prover webpage ( recommended)