饱和约束Horn子句的符号模型构建
摘要：用层次有序解析饱和的子句集不能提供一个一般情况下可以有效查询的模型表示。它们只提供存在模型的保证。我们提出了一种对饱和约束Horn子句进行有效符号化模型构建的方法。约束是在线性算术中进行的，一阶部分限制在无函数的语言中。该模型在有限时间内构建，并且可以有效地针对模型对非对地子句进行评估。此外，我们证明了我们的模型构建产生了最小模型。
作者：Martin Bromberger, Lorenz Leutgeb, Christoph Weidenbach
论文ID：2305.05064
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-07-25