Carnegie Mellon University
Browse
file.pdf (274.74 kB)

Focus-preserving Embeddings of Substructural Logics in Intuitionistic Logic

Download (274.74 kB)
journal contribution
posted on 2005-10-01, 00:00 authored by Jason Reed, Frank Pfenning
We present a method of embedding substructural logics into ordinary first-order intuitionistic logic. This embedding is faithful in a very strong sense: not only does it preserve provability of sequents under translation, but it also preserves sets of proofs — and the focusing structure of those proofs — up to isomorphism. Examples are given for the cases of intuitionistic linear logic and ordered logic, and indeed we can use our method to derive a correct focusing system for ordered logic. Potential applications lie in logic programming, theorem proving, and logical frameworks for substructural logics where focusing is crucial for the underlying proof theory.

History

Date

2005-10-01

Usage metrics

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC