走向图变换在直觉线性逻辑中的嵌入
计算机科学中的逻辑
2009-12-01 v1
摘要
线性逻辑已被证明能够在单一的声明式框架中嵌入基于重写的方法和进程演算。在本文中，我们探索将双推出图变换嵌入量化线性逻辑，从而在图与变换一方，以及公式与证明项另一方之间，建立一种Curry-Howard风格的同构。通过用线性蕴涵表示规则与图的可达性，并用张量积建模图与变换的并行复合，我们获得了一种语言，能够将图变换系统及其计算进行编码，并对它们的性质进行推理。
引用
@article{arxiv.0911.5525,
title = {Towards an embedding of Graph Transformation in Intuitionistic Linear Logic},
author = {Paolo Torrini and Reiko Heckel},
journal= {arXiv preprint arXiv:0911.5525},
year = {2009}
}