Accession Number : ADA476798


Title :   From Indexed Lax Logic to Intuitionistic Logic


Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE


Personal Author(s) : Garg, Deepak ; Tschantz, Michael C


Full Text : https://apps.dtic.mil/dtic/tr/fulltext/u2/a476798.pdf


Report Date : 07 Jan 2008


Pagination or Media Count : 37


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.


Descriptors :   *COMPUTER LOGIC , TRANSLATIONS , SYNTAX


Subject Categories : Computer Programming and Software


Distribution Statement : APPROVED FOR PUBLIC RELEASE