© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Proof Search in Lax Logic
Jacob M. Howe
Mathematical Structures in Computer Science, 11(4):182-196, August 2001.Abstract
A Gentzen sequent calculus for Lax Logic is presented, the proofs in which naturally correspond 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, one which uses a history mechanism in order to give a decision procedure for propositional Lax Logic.
Download publication 87 kbytesBibtex Record
@article{1219,
author = {Jacob M. Howe},
title = {Proof {S}earch in {L}ax {L}ogic},
month = {August},
year = {2001},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2001/1219},
publication_type = {article},
submission_id = {18232_996074590},
journal = {Mathematical Structures in Computer Science},
volume = {11},
number = {4},
publisher = {Cambridge University Press},
}