Coq中的Trakhtenbrot定理：通过构造性视角看有限模型论
计算机科学中的逻辑
2023-06-22 v5 计算与语言
逻辑
摘要
我们在依赖类型论的构造性设定中研究有限一阶可满足性（FSAT）。采用可枚举性与可判定性的综合刻画，我们给出了依赖于一阶非逻辑符号签名的FSAT的完整分类。一方面，我们的研究聚焦于Trakhtenbrot定理，该定理指出只要签名包含至少一个二元关系符号，FSAT就是不可判定的。我们的证明通过从Post对应问题出发的许多一归约链进行。另一方面，我们确立了单元一阶逻辑（即签名仅包含至多一元的函数和关系符号）的FSAT的可判定性，以及任意可枚举签名的FSAT的可枚举性。为展示Trakhtenbrot定理的一个应用，我们将归约链继续，给出从FSAT到分离逻辑的许多一归约。我们的所有结果都在一个不断增长的合成不可判定性证明的Coq库框架中实现了机械化。
引用
@article{arxiv.2104.14445,
title = {Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens},
author = {Dominik Kirst and Dominique Larchey-Wendling},
journal= {arXiv preprint arXiv:2104.14445},
year = {2023}
}
备注
arXiv admin note: substantial text overlap with arXiv:2004.07390