Embedding Proof Problems into Query-answering Problems and Problem Solving by Equivalent Transformation

Kiyoshi Akama, Ekawit Nantajeewarawat

2013

Abstract

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.

Paper Citation

in Harvard Style

Akama K. and Nantajeewarawat E. (2013). Embedding Proof Problems into Query-answering Problems and Problem Solving by Equivalent Transformation . In Proceedings of the International Conference on Knowledge Engineering and Ontology Development - Volume 1: KEOD, (IC3K 2013) ISBN 978-989-8565-81-5, pages 253-260. DOI: 10.5220/0004546202530260

in Bibtex Style

@conference{keod13,
author={Kiyoshi Akama and Ekawit Nantajeewarawat},
title={Embedding Proof Problems into Query-answering Problems and Problem Solving by Equivalent Transformation},
booktitle={Proceedings of the International Conference on Knowledge Engineering and Ontology Development - Volume 1: KEOD, (IC3K 2013)},
year={2013},
pages={253-260},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0004546202530260},
isbn={978-989-8565-81-5},
}

in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Knowledge Engineering and Ontology Development - Volume 1: KEOD, (IC3K 2013)
TI - Embedding Proof Problems into Query-answering Problems and Problem Solving by Equivalent Transformation
SN - 978-989-8565-81-5
AU - Akama K.
AU - Nantajeewarawat E.
PY - 2013
SP - 253
EP - 260
DO - 10.5220/0004546202530260