Syntax of Linear Logic Prover

Naoyuki Tamura
Department of CS, Kobe University

Introduction

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.

Syntax

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.

References

1
J.-Y. Girard: Linear Logic. Theoretical Computer Science, 50:1--102, 1987.
2
J.-Y. Girard, P. Taylor, Y. Lafont: Proofs and Types. Cambridge University Press, 1988.
3
A. S. Troelstra: Lectures on Linear Logic. CSLI Lecture Notes No.29, 1992.

About this document ...

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


Naoyuki Tamura
Tue Feb 18 11:57:20 JST 1997