Coq中的Trakhtenbrot定理：有限模型理论的构造性方法
计算机科学中的逻辑
2020-04-17 v1 计算与语言
逻辑
摘要
我们在依赖类型理论的构造性环境中研究有限一阶可满足性（FSAT）。借助可枚举性与可判定性的综合刻画（synthetic accounts），我们依据非逻辑符号的一阶签名对FSAT给出了完整分类。一方面，我们的工作聚焦于Trakhtenbrot定理，该定理指出只要签名包含至少一个二元关系符号，FSAT便是不可判定的。我们的证明通过从Post对应问题出发的许多一归约（many-one reduction）链进行。另一方面，我们确立了单元一阶逻辑（即签名仅包含至多一元函数与关系符号）中FSAT的可判定性，以及任意可枚举签名下FSAT的可枚举性。我们的所有结果均在不断增长的合成不可判定性证明的Coq库框架中机械化。
引用
@article{arxiv.2004.07390,
title = {Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory},
author = {Dominik Kirst and Dominique Larchey-Wendling},
journal= {arXiv preprint arXiv:2004.07390},
year = {2020}
}