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

• Variables:
  Please use uppercase letters (e.g. X, Y, X0, ...).
• Constants:
  Please use lowercase letters or numbers (e.g. a, b, 1, ...).
• Function symbols:
  Please use lowercase letters (e.g. a, b, c, ...).
• Predicate symbols:
  Please use lowercase letters (e.g. a, b, c, ...).

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