基于重写逻辑的顺序系统规约、证明搜索与元证明方法
计算机科学中的逻辑
2021-01-11 v1 逻辑
摘要
本文提出了一种基于算法的方法，用于证明命题顺序系统的归纳性质，如可接纳性、可逆性、割消去和恒等展开。尽管这些结构性质在一般情况下是不可判定的，但它们在证明论中至关重要，因为它们能够减少证明搜索的工作量，并进一步用作获取其他元结果（如一致性）的脚手架。这些算法——利用了重写逻辑元逻辑框架，并使用基于重写和收窄的推理——在全文中有详细解释并辅以示例说明。它们已在 L-Framework 中完全机械化，从而既提供了形式规约语言，又提供了现成的证明搜索算法机械化，并附带用于证明对象系统定理和元定理的半判定过程。如文中案例研究所示，L-Framework 在多个命题顺序系统（包括单结论与多结论直觉主义逻辑、经典逻辑、经典线性逻辑及其双系统、直觉主义线性逻辑以及正规模态逻辑）上使用时实现了高度的自动化。
引用
@article{arxiv.2101.03113,
title = {A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems},
author = {Carlos Olarte and Elaine Pimentel and Camilo Rocha},
journal= {arXiv preprint arXiv:2101.03113},
year = {2021}
}