## Abstract / Description of output

We construct the exponential graph of a proof π in (second order) linear logic, an artefact displaying the interdependencies of exponentials in π. Within this graph superfluous exponentials are defined, the removal of which is shown to yield a correct proof π▹ with essentially the same set of reductions.

Applications to intuitionistic and classical proofs are given by means of reduction-preserving embeddings into linear logic.

The last part of the paper puts things the other way round, and defines families of linear logics in which exponential dependencies are ruled by a given graph. We sketch some work in progress and possible applications.

Applications to intuitionistic and classical proofs are given by means of reduction-preserving embeddings into linear logic.

The last part of the paper puts things the other way round, and defines families of linear logics in which exponential dependencies are ruled by a given graph. We sketch some work in progress and possible applications.

Original language | English |
---|---|

Title of host publication | Computational Logic and Proof Theory |

Subtitle of host publication | Third Kurt Gödel Colloquium, KGC'93 Brno, Czech Republic, August 24–27, 1993 Proceedings |

Editors | Georg Gottlob, Alexander Leitsch, Daniele Mundici |

Publisher | Springer Berlin Heidelberg |

Pages | 159-171 |

Number of pages | 13 |

Volume | 713 |

ISBN (Electronic) | 978-3-540-47943-7 |

ISBN (Print) | 978-3-540-57184-1 |

DOIs | |

Publication status | Published - 1993 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer Berlin Heidelberg |

Volume | 713 |