一阶理论的可满足性模选择完整触发
摘要：如果T是一个没有除量词实例化之外的理论求解器的SMT求解器。给定一组通过分辨率饱和的一阶子句集S（具有有效的文字选择函数），我们证明如果其触发函数与文字选择函数相同，则T是完备的。因此，如果T以一个地面模型G停机，则G可以扩展为S理论中的一个模型。另外，对于适当的排序，如果每个子句中选择所有的最大文字，则T将在G上停机，因此它是S理论的一个决策过程。此外，对于适当的排序，如果所有子句都是Horn子句，或者所有子句都是2SAT子句，则T在多项式时间内解决了S理论。
作者：Christopher Lynch and Stephen Miner
论文ID：2306.09436
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22