Naoyuki Tamura
Department of CS, Kobe University
This program searches a cut-free proof of the given two-sided sequent of 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.
Formulas should be written in Prolog syntax (precisely speaking, SICStus Prolog is used).
Logical operators should be written as follows. Please note that 0 and are different from Girard's original notation because Troelstra's notation is used here [3].
Operator precedences are defined as follows. Smaller precedence value means narrower scope.
To write a sequent, please use --> for the arrow and [] for the empty sequence. The following shows the examples.
Syntax of Linear Logic Prover
This document was generated using the LaTeX2HTML translator Version 95 (Thu Jan 19 1995) Copyright © 1993, 1994, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
The command line arguments were:
latex2html -split 0 doc.tex.
The translation was initiated by Naoyuki Tamura on Tue Feb 18 11:57:20 JST 1997