Proof Search in Lax Logic

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.