A Bottom-Up Algorithm for Solving Query-Answering Problems

Meaning-preserving Skolemization is essential for development of a correct and efficient method of solving query-answering problems. It requires global existential quantifications of function variables, which in turn require an extension of the space of first-order formulas. This paper proposes a bottom-up algorithm for computing a set of models that sufficiently represents the set of all models of a given clause set in the extended formula space. This algorithm provides a correct method for solving query-answering problems that include unrestricted use of universal and existential quantifications in problem representation.