2014 | OriginalPaper | Chapter
Equivalent Transformation in an Extended Space for Solving Query-Answering Problems
Authors : Kiyoshi Akama, Ekawit Nantajeewarawat
Published in: Intelligent Information and Database Systems
Publisher: Springer International Publishing
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
A query-answering problem (QA problem) is concerned with finding all ground instances of a query atomic formula that are logical consequences of a given logical formula describing the background knowledge of the problem. Based on the equivalent transformation (ET) principle, we propose a general framework for solving QA problems on first-order logic. To solve such a QA problem, the first-order formula representing its background knowledge is converted by meaning-preserving Skolemization into a set of clauses typically containing global existential quantifications of function variables. The obtained clause set is then transformed successively using ET rules until the answer set of the original problem can be readily derived. Many ET rules are demonstrated, including rules for unfolding clauses, for resolution, for dealing with function variables, and for erasing independent satisfiable atomic formulas. Application of the proposed framework is illustrated.