A Delayed Splitting Bottom-Up Procedure for Model Generation

Abstract

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 extended space of logical formulas. This paper proposes a bottom-up procedure for computing a set of models that sufficiently represents the set of all models of a given clause set in the extended formula space. Instantiations of function variables often result in generation of infinitely many models. To overcome the difficulty, a model-making pattern is introduced for representing a possibly infinite number of models, and such a pattern is split as late as possible. The proposed procedure provides a method for solving query-answering problems that include unrestricted use of universal and existential quantifications.