 |
    |
A Delayed Splitting Bottom-Up Procedure for Model Generation
Kiyoshi Akama1 and Ekawit Nantajeewarawat2
1Information Initiative Center, Hokkaido University, Hokkaido, Japan
akama@iic.hokudai.ac.jp
2Computer Science Program, Sirindhorn International Institute of Technology, Thammasat University, Pathumthani, Thailand
ekawit@siit.tu.ac.th
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.
Keywords: Query-answering problems, automated reasoning, bottom-up computation, meaning-preserving Skolemization
LNAI 7691, p. 481 ff.
lncs@springer.com
© Springer-Verlag Berlin Heidelberg 2012