Solving Query-Answering Problems with Constraints for Function Variables

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) solution method, a general framework for solving QA problems on first-order logic has been proposed, where a first-order formula representing 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. In this paper, we extend the space of clauses by introducing constraints and invent three ET rules for simplifying problem descriptions by using interaction between clauses and constraints. This extension provides a general solution for a larger class of QA problems.