CMU-CS-07-167
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-07-167

From Indexed Lax Logic to Intuitionistic Logic

Deepak Garg, Michael Carl Tschantz

January 2008

CMU-CS-07-167.pdf

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 reports@cs.cmu.edu