| Computer Science Laboratory | |
| Contact | |
 | People at CSL |
| Projects at CSL |
| Research Programs |
| Division Home | |
 Linearizing Intuitionistic Implication by Dr. Patrick Lincoln, Dr. Natarajan Shankar & Andre Scedrov. Abstract An embedding of the implicational propositional intuitionistic logic (IlL) into the nonmodal fragment of intuitionistic linear logic (IMALL) is given. The embedding preserves cut-free proofs in a proof system that is a variant of IlL. The embedding is efficient and provides an alternative proof of the PSPACE-hardness of IMALL. It exploits several proof-theoretic properties of intuitionistic implication that analyze the use of re sources in IlL proofs.Files |
||||
About Us 
R&D Divisions
Careers
Newsroom
Contact Us
©
2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy