Mathematical Structures in Computer Science

Table of Contents - 2001 - Volume 11, Issue 04  

Special Issue: Modalities in Type Theory

Proof search in Lax Logic

JACOB M. HOWE a1 1
a1 Computing Laboratory, University of Kent, Canterbury CT2 7NF, England

Abstract

A Gentzen sequent calculus for Lax Logic is presented, the proofs in which correspond naturally in a 1–1 way to the normal natural deductions for the logic. The propositional fragment of this calculus is used as the basis for another calculus that uses a history mechanism in order to give a decision procedure for propositional Lax Logic.

(Received September 20 1999)
(Revised June 13 2000)


Footnotes

1 This work was partly supported by EPSRC grant GR/MO8769