面向集合论无量词片段的已验证 tableau 证明器
计算机科学中的逻辑
2023-07-04 v2
摘要
我们使用 Isabelle/HOL 验证针对带单元素集的多层三段论（简称 MLSS）这一集合论无量词片段的先进决策过程。我们形式化了其语法与语义，以及针对它的一个可靠且完备的 tableau 演算。我们还给出了一个可执行的决策过程规范，该过程穷尽地应用演算规则，并证明其终止性。此外，我们用一个轻量级类型系统扩展了该演算，为将该过程集成到 Isabelle/HOL 中铺平了道路。
引用
@article{arxiv.2209.14133,
title = {Towards a Verified Tableau Prover for a Quantifier-Free Fragment of Set Theory},
author = {Lukas Stevens},
journal= {arXiv preprint arXiv:2209.14133},
year = {2023}
}