通过原子流控制深推演中的规范化
逻辑
2015-07-01 v3 计算机科学中的逻辑
摘要
我们引入“原子流”：它们是通过对推导中原子出现情况进行追踪并忽略逻辑结构而获得的图。我们研究了原子流的简单操作，这些操作对应于推导上的复杂归约。这使我们能够为命题逻辑证明一个新的且非常通用的规范化定理，其中消切作为特例包含在内。我们在深推演框架下进行操作，该框架比其他句法范式更通用，且其中的规范化更难控制。我们认为原子流是规范化理论的一项重大技术进步，因为：1) 它们所支持的技术在很大程度上独立于句法；2) 事实上，它在很大程度上独立于逻辑推理规则；3) 它们构成了一种强大的几何形式体系，比句法更直观。
引用
@article{arxiv.0709.1205,
title = {Normalisation Control in Deep Inference via Atomic Flows},
author = {Alessio Guglielmi and Tom Gundersen},
journal= {arXiv preprint arXiv:0709.1205},
year = {2015}
}