Computer Science Department
School of Computer Science, Carnegie Mellon University


From Indexed Lax Logic to Intuitionistic Logic

Deepak Garg, Michael Carl Tschantz

January 2008


Keywords: Lax logic, affirmations, logical transformations

We present translations from a logic with indexed lax modalities to first-order intuitionistic logic and intuitionistic linear logic. These translations rely on a continuation passing style encoding for the lax modalities. We show that our translations preserve provability of formulas.

36 pages

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by