From Indexed Lax Logic to Intuitionistic Logic

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 07, 2008
Accession Number
ADA476798

Entities

People

  • Deepak Garg
  • Michael C. Tschantz

Organizations

  • Carnegie Mellon University

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Air Force Research Laboratories
  • Calculus
  • Coding
  • Computer Access Control
  • Computer Programming
  • Computer Science
  • Computers
  • Control Systems
  • Cybersecurity
  • Entry Control Systems
  • Inversion
  • Judgment
  • Military Research
  • New York
  • Theoretical Computer Science
  • Translations

Readers

  • Computational Linguistics
  • Computer Engineering