论文标题
一些模型的否定理论
Some Model Theory of Guarded Negation
论文作者
论文摘要
受保护的否定片段（GNFO）是一阶逻辑的片段，包含所有积极的存在公式，可以表达基本模态逻辑和许多描述逻辑的一阶翻译，以及数据库中出现的许多句子。已经表明，GNFO的语法足够限制，因此诸如有效性和可满足性之类的计算问题仍然是可决定的。这表明，尽管具有表达能力，但GNFO公式仍适合新颖的优化。在本文中，我们研究了GNFO公式的模型理论。我们的结果包括用于GNFO的有效保存定理，有效的Craig插值和Beth的可确定性结果，以及在非常有限的逻辑中就大类GNFO句子表达查询的某些答案的能力。 本文的本版本包含有关结果的简化和更正版本，这些版本是从一组地面事实中构成一个结合查询的，以及由特殊形式的gnfo句子组成的理论（“依赖关系”）。
The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this paper we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics. This version of the paper contains streamlined and corrected versions of results concerning entailment of a conjunctive query from a set of ground facts and a theory consisting of GNFO sentences of a special form ("dependencies").
