© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Proof Search in Lax Logic
Jacob M. Howe
Technical Report 14-99, University of Kent, July 1999.Abstract
A Gentzen sequent calculus for Lax Logic is presented, the proofs in which naturally correspond in a 1--1 way with the normal natural deductions for the logic. The propositional fragment of this calculus is then used a basis for another calculus, one which uses a history mechanism in order to give a decision procedure for propositional Lax Logic.
Download publication 70 kbytesBibtex Record
@techreport{877,
author = {Howe, Jacob M.},
title = {Proof {S}earch in {L}ax {L}ogic},
month = {July},
year = {1999},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1999/877},
institution = {University of Kent},
number = {14-99},
}