View Full Document

From Indexed Lax Logic to Intuitionistic Logic



View the full content.
View Full Document
View Full Document

2 views

Unformatted text preview:

From Indexed Lax Logic to Intuitionistic Logic Deepak Garg1 Michael Carl Tschantz2 January 2008 CMU CS 07 167 School of Computer Science Carnegie Mellon University Pittsburgh PA 15213 Abstract 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 1 This author was partially sponsored by the Air Force Research Laboratory under grant no FA87500720028 The views and conclusions contained in this document are those of the author and should not be interpreted as representing official policies either expressed or implied of any sponsoring institution the U S government or any other entity 2 This author was partially sponsored by the Army Research Office through grant number DAAD19 02 1 0389 Perpetually Available and Secure Information Systems to Carnegie Mellon University s CyLab and by a generous gift from the Hewlett Packard Corporation The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies either expressed or implied of any sponsoring institution the U S government or any other entity Keywords Lax Logic Affirmations Logical Transformations 1 Introduction Lax logic is a modal logic extending intuitionistic propositional logic with a single modality lax A satisfying the following axioms A A A A A B A B In this report we describe two simple translations of lax logic with multiple modalities a first order translation into first order intuitionistic logic and a linear translation into intuitionistic linear logic We show that our translations preserve provability The essence of these translations is a continuation passing style CPS encoding of the lax modality Background In its propositional form lax logic was introduced by Mendler et al FM97 as a means of



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view From Indexed Lax Logic to Intuitionistic Logic and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view From Indexed Lax Logic to Intuitionistic Logic and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?