使用 Z3 验证线性逻辑片段中的推理
计算机科学中的逻辑
2023-09-26 v1
摘要
线性逻辑是作为经典逻辑与直觉主义逻辑精炼而提出的一种亚结构逻辑，在编程语言、博弈语义与量子物理中有应用。我们提出一种支持使用自动定理证明验证逻辑推理规则的 Gentzen 式线性逻辑相继式模板。具体而言，我们使用 Z3 定理证明器 [8] 基于一组被假定为有效的推理规则来检验目标推理规则。为演示该方法，我们将其应用于验证线性逻辑两个不同片段的若干导出推理规则：MLL+Mix（乘性线性逻辑扩展以 Mix 规则）与 MILL（乘性直觉主义线性逻辑）。
引用
@article{arxiv.2309.13796,
title = {Using Z3 to Verify Inferences in Fragments of Linear Logic},
author = {Alen Docef and Radu Negulescu and Mihai Prunescu},
journal= {arXiv preprint arXiv:2309.13796},
year = {2023}
}
备注
In Proceedings FROM 2023, arXiv:2309.12959