Model-Intersection Problems with Existentially Quantified Function Variables: Formalization and a Solution Schema
Model-Intersection Problems with Existentially Quantified Function Variables: Formalization and a Solution Schema
复制标题
DOI：
10.5220/0006056800520063
复制
发表时间：
2016-11
期刊：
影响因子：
--
通讯作者：
K. Akama;Ekawit Nantajeewarawat
中科院分区：
文献类型：
--
作者：
K. Akama;Ekawit Nantajeewarawat
内置约束原子在知识表示中起着非常重要的作用，在实际应用中是不可缺少的。在使用一阶公式形式化逻辑问题时，将内置约束原子与用户定义原子一起使用是非常自然的。然而，在固有约束原子存在的情况下，常规的斯科勒姆化一般既不保留给定一阶公式的可满足性，也不保留给定一阶公式的逻辑意义，这促使我们走出常规的斯科勒姆化和通常的一阶公式空间。针对一阶公式可能具有内建约束原子的证明问题和问答问题，提出了一般的解法。通过使用新的保留意义的Skolemization，我们将所有证明问题和所有QA问题映射到扩展子句空间上的一类新的模型相交（MI）问题，其中子句在某种意义上是“高阶”的，因为它们不仅包含内置的约束原子，还包含函数变量。我们提出了用等效变换（ET）解决这类MI问题的一般模式，其中问题通过使用ET规则的重复简化来解决。说明了该解决方案模式的正确性。由于本文中的MI问题形成了一个非常大的逻辑问题类别，因此该理论也有助于为许多类别的逻辑问题提供解决方案。
Built-in constraint atoms play a very important role in knowledge representation and are indispensable for practical applications. It is very natural to use built-in constraint atoms together with user-defined atoms when formalizing logical problems using first-order formulas. In the presence of built-in constraint atoms, however, the conventional Skolemization in general preserves neither the satisfiability nor the logical meaning of a given first-order formula, motivating us to step outside the conventional Skolemization and the usual space of first- order formulas. We propose general solutions for proof problems and query-answering (QA) problems on first-order formulas possibly with built-in constraint atoms. We map, by using new meaning-preserving Skolemization, all proof problems and all QA problems, preserving their answers, into a new class of model-intersection (MI) problems on an extended clause space, where clauses are in a sense ``higher-order'' since they may contain not only built-in constraint atoms but also function variables. We propose a general schema for solving this class of MI problems by equivalent transformation (ET), where problems are solved by repeated simplification using ET rules. The correctness of this solution schema is shown. Since MI problems in this paper form a very large class of logical problems, this theory is also useful for inventing solutions for many classes of logical problems.