Embedding Proof Problems into Query-answering Problems and Problem Solving by Equivalent Transformation
Embedding Proof Problems into Query-answering Problems and Problem Solving by Equivalent Transformation
复制标题
将证明问题嵌入到问答问题中并通过等价变换解决问题
DOI：
10.5220/0004546202530260
复制
发表时间：
2018
影响因子：
3
通讯作者：
Ekawit Nantajeewarawat
中科院分区：
文献类型：
--
作者：
K. Akama;Ekawit Nantajeewarawat
一个证明问题是一个关于检查一个逻辑公式是否是另一个逻辑公式的逻辑结果的“是/否”问题，而一个查询-回答问题（QA问题）是一个关于寻找一个查询原子公式的所有基础实例的“所有答案寻找”问题，这些基础实例是给定逻辑公式的逻辑结果。为了在这两个问题类之间建立精确的关系，引入了嵌入映射的概念。当一个问题类可以以低计算成本嵌入到另一个问题类中时，前一类可以被视为后一类的子类，因此，前一类中的问题可以通过用于解决后一类中的问题的方法来解决。从证明问题到QA问题的低成本嵌入映射的建设被证明。通过这样的嵌入，证明问题可以使用用于解决QA问题的过程来解决。提出了一种基于等价变换原理的求解QA问题的方法。应用程序的两个问题类的说明。
A proof problem is a “yes/no” problem concerning with checking whether one logical formula is a logical consequence of another logical formula, while a query-answering problem (QA problem) is an “all-answers finding” problem concerning with finding all ground instances of a query atomic formula that are logical consequences of a given logical formula. In order to establish a precise relation between these two problem classes, the concept of an embedding mapping is introduced. When one problem class can be embedded into another problem class at low computational cost, the former class can be regarded as a subclass of the latter class and, consequently, problems in the former class can be solved through a method for solving problems in the latter one. Construction of low-cost embedding mappings from proof problems to QA problems is demonstrated. By such embedding, proof problems can be solved using a procedure for solving QA problems. A procedure for solving QA problems based on the equivalent transformation principle is presented. Application of the procedure to the two problem classes is illustrated.