从饱和嵌入测试到显式算法
摘要：量词消除定理显示某个理论中的每个公式等同于一个特定形式的公式 -- 通常是一个无量词的公式，有时是在扩展语言中。模型论嵌入测试是一种常用的证明此类结果的工具，而不提供明确的算法。 我们解释了如何将证明挖掘方法适应于嵌入测试，并提供了两个具体例子，给出了代数和实闭域理论的算法，其中有一个有一个特殊的小子群，对应于van den Dries和G"unaydin给出的嵌入测试证明。
作者：Henry Towsner
论文ID：2306.12239
分类：Logic
分类简称：math.LO
提交时间：2023-07-10