A General Schema for Solving Model-Intersection Problems on a Specialization System by Equivalent Transformation
A General Schema for Solving Model-Intersection Problems on a Specialization System by Equivalent Transformation
复制标题
DOI：
10.5220/0005597000380049
复制
发表时间：
2015-11
期刊：
影响因子：
--
通讯作者：
K. Akama;Ekawit Nantajeewarawat
中科院分区：
文献类型：
--
作者：
K. Akama;Ekawit Nantajeewarawat
模型交集问题（MI 问题）是一对子句集和一个出口映射。我们在专业化系统上定义 MI 问题，其中包括许多有用的逻辑问题类别，例如一阶逻辑的证明问题以及纯 Prolog 和演绎数据库中的查询回答 (QA) 问题。本文提出的理论通过（i）公理化和（ii）等价变换阐明了许多类逻辑问题的表示和计算的中心和基本结构。该理论中的子句是基于抽象原子和对其进行抽象操作而构造的，可以用具体语法来表示问题的许多具体子类。通过重复应用许多等价变换规则可以实现各种计算，从而允许许多可能的计算过程，例如基于解析和展开的计算过程。该理论对于发明新类别逻辑问题的解决方案也很有用。
A model-intersection problem (MI problem) is a pair of a set of clauses and an exit mapping. We define MI problems on specialization systems, which include many useful classes of logical problems, such as proof problems on first-order logic and query-answering (QA) problems in pure Prolog and deductive databases. The theory presented in this paper makes clear the central and fundamental structure of representation and computation for many classes of logical problems by (i) axiomatization and (ii) equivalent transformation. Clauses in this theory are constructed based on abstract atoms and abstract operation on them, which can be used for representation of many specific subclasses of problems with concrete syntax. Various computation can be realized by repeated application of many equivalent transformation rules, allowing many possible computation procedures, for instance, computation procedures based on resolution and unfolding. This theory can also be useful for inventing solutions for new classes of logical problems.